1 /-
2 Copyright (c) 2019 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison
5 -/
6 import data.equiv.basic logic.embedding
src └──────────────┘ └─────────────┘
7 import data.nat.cast
src └───────────┘
8 import data.finset data.fintype
src └─────────┘ └──────────┘
9
10 /-!
11 # Combinatorial (pre-)games.
12
13 The basic theory of combinatorial games, following Conway's book `On Numbers and Games`. We
14 construct "pregames", define an ordering and arithmetic operations on them, then show that the
15 operations descend to "games", defined via the equivalence relation `p ≈ q ↔ p ≤ q ∧ q ≤ p`.
16
17 The surreal numbers will be built as a quotient of a subtype of pregames.
18
19 A pregame (`pgame` below) is axiomatised via an inductive type, whose sole constructor takes two
20 types (thought of as indexing the the possible moves for the players Left and Right), and a pair of
21 functions out of these types to `pgame` (thought of as describing the resulting game after making a
22 move).
23
24 Combinatorial games themselves, as a quotient of pregames, are constructed in `game.lean`.
25
26 ## Conway induction
27
28 By construction, the induction principle for pregames is exactly "Conway induction". That is, to
29 prove some predicate `pgame → Prop` holds for all pregames, it suffices to prove that for every
30 pregame `g`, if the predicate holds for every game resulting from making a move, then it also holds
31 for `g`.
32
33 While it is often convenient to work "by induction" on pregames, in some situations this becomes
34 awkward, so we also define accessor functions `left_moves`, `right_moves`, `move_left` and
35 `move_right`. There is a relation `subsequent p q`, saying that `p` can be reached by playing some
36 non-empty sequence of moves starting from `q`, an instance `well_founded subsequent`, and a local
37 tactic `pgame_wf_tac` which is helpful for discharging proof obligations in inductive proofs relying
38 on this relation.
39
40 ## Order properties
41
42 Pregames have both a `≤` and a `<` relation, which are related in quite a subtle way. In particular,
43 it is worth noting that in Lean's (perhaps unfortunate?) definition of a `preorder`, we have
44 `lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a)`, but this is _not_ satisfied by the usual
45 `≤` and `<` relations on pregames. (It is satisfied once we restrict to the surreal numbers.) In
46 particular, `<` is not transitive; there is an example below showing `0 < star ∧ star < 0`.
47
48 We do have
49 ```
50 theorem not_le {x y : pgame} : ¬ x ≤ y ↔ y < x := ...
51 theorem not_lt {x y : pgame} : ¬ x < y ↔ y ≤ x := ...
52 ```
53
54 The statement `0 ≤ x` means that Left has a good response to any move by Right; in particular, the
55 theorem `zero_le` below states
56 ```
57 0 ≤ x ↔ ∀ j : x.right_moves, ∃ i : (x.move_right j).left_moves, 0 ≤ (x.move_right j).move_left i
58 ```
59 On the other hand the statement `0 < x` means that Left has a good move right now; in particular the
60 theorem `zero_lt` below states
61 ```
62 0 < x ↔ ∃ i : left_moves x, ∀ j : right_moves (x.move_left i), 0 < (x.move_left i).move_right j
63 ```
64
65 The theorems `le_def`, `lt_def`, give a recursive characterisation of each relation, in terms of
66 themselves two moves later. The theorems `le_def_lt` and `lt_def_lt` give recursive
67 characterisations of each relation in terms of the other relation one move later.
68
69 We define an equivalence relation `equiv p q ↔ p ≤ q ∧ q ≤ p`. Later, games will be defined as the
70 quotient by this relation.
71
72 ## Algebraic structures
73
74 We next turn to defining the operations necessary to make games into a commutative additive group.
75 Addition is defined for $x = \{xL | xR\}$ and $y = \{yL | yR\}$ by $x + y = \{xL + y, x + yL | xR +
76 y, x + yR\}$. Negation is defined by $\{xL | xR\} = \{-xR | -xL\}$.
77
78 The order structures interact in the expected way with addition, so we have
79 ```
80 theorem le_iff_sub_nonneg {x y : pgame} : x ≤ y ↔ 0 ≤ y - x := sorry
81 theorem lt_iff_sub_pos {x y : pgame} : x < y ↔ 0 < y - x := sorry
82 ```
83
84 We show that these operations respect the equivalence relation, and hence descend to games. At the
85 level of games, these operations satisfy all the laws of a commutative group. To prove the necessary
86 equivalence relations at the level of pregames, we introduce the notion of a `relabelling` of a
87 game, and show, for example, that there is a relabelling between `x + (y + z)` and `(x + y) + z`.
88
89 ## Future work
90 * The theory of dominated and reversible positions, and unique normal form for short games.
91 * Analysis of basic domineering positions.
92 * Impartial games, nim, and the Sprague-Grundy theorem.
93 * Hex.
94 * Temperature.
95 * The development of surreal numbers, based on this development of combinatorial games, is still
96 quite incomplete.
97
98 ## References
99
100 The material here is all drawn from
101 * [Conway, *On numbers and games*][conway2001]
102
103 An interested reader may like to formalise some of the material from
104 * [Andreas Blass, *A game semantics for linear logic*][MR1167694]
st ┴
105 * [André Joyal, *Remarques sur la théorie des jeux à deux personnes*][joyal1997]
st ┴
106 -/
107
108 universes u
109
110 /-- The type of pre-games, before we have quotiented
111 by extensionality. In ZFC, a combinatorial game is constructed from
112 two sets of combinatorial games that have been constructed at an earlier
113 stage. To do this in type theory, we say that a pre-game is built
114 inductively from two families of pre-games indexed over any type
115 in Type u. The resulting type `pgame.{u}` lives in `Type (u+1)`,
116 reflecting that it is a proper class in ZFC. -/
117 inductive pgame : Type (u+1)
118 | mk : ∀ α β : Type u, (α → pgame) → (β → pgame) → pgame
id └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴
119
120 namespace pgame
121
122 /-- Construct a pre-game from list of pre-games describing the available moves for Left and Right. -/
123 -- TODO provide some API describing the interaction with `left_moves`, `right_moves`, `move_left` and `move_right` below.
124 -- TODO define this at the level of games, as well, and perhaps also for finsets of games.
125 def of_lists (L R : list pgame.{0}) : pgame.{0} :=
id └──┘ └───┘ └───┘
src └──┘ └───┘ └───┘
typ └──┘ └───┘ └───┘
doc └───┘ └───┘
126 pgame.mk (fin L.length) (fin R.length) (λ i, L.nth_le i.val i.is_lt) (λ j, R.nth_le j.val j.is_lt)
id └──────┘ └─┘ ┴└─────┘ └─┘ ┴└─────┘ ┴ ┴└─────┘ ┴└──┘ ┴└────┘ ┴ ┴└─────┘ ┴└──┘ ┴└────┘
src └──────┘ └─┘ └─────┘ └─┘ └─────┘ └─────┘ └──┘ └────┘ └─────┘ └──┘ └────┘
typ └──────┘ └─┘ ┴└─────┘ └─┘ ┴└─────┘ ┴ ┴└─────┘ ┴└──┘ ┴└────┘ ┴ ┴└─────┘ ┴└──┘ ┴└────┘
127
128 /-- The indexing type for allowable moves by Left. -/
129 def left_moves : pgame → Type u
id └───┘ ┴
src └───┘
typ └───┘ ┴
doc └───┘
130 | (mk l _ _ _) := l
id └┘ ┴
src └┘
typ └┘ ┴
131 /-- The indexing type for allowable moves by Right. -/
132 def right_moves : pgame → Type u
id └───┘ ┴
src └───┘
typ └───┘ ┴
doc └───┘
133 | (mk _ r _ _) := r
id └┘ ┴
src └┘
typ └┘ ┴
134
135 /-- The new game after Left makes an allowed move. -/
136 def move_left : Π (g : pgame), left_moves g → pgame
id ┴ └───┘ └────────┘ ┴ └───┘
src └───┘ └────────┘ └───┘
typ ┴ └───┘ └────────┘ ┴ └───┘
doc └───┘ └────────┘ └───┘
137 | (mk l _ L _) i := L i
id └┘ ┴ ┴
src └┘
typ └┘ ┴ ┴
138 /-- The new game after Right makes an allowed move. -/
139 def move_right : Π (g : pgame), right_moves g → pgame
id ┴ └───┘ └─────────┘ ┴ └───┘
src └───┘ └─────────┘ └───┘
typ ┴ └───┘ └─────────┘ ┴ └───┘
doc └───┘ └─────────┘ └───┘
140 | (mk _ r _ R) j := R j
id └┘ ┴ ┴
src └┘
typ └┘ ┴ ┴
141
142 @[simp] lemma left_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).left_moves = xl := rfl
id └┘ └┘ └┘ └┘ └───┘ └────────┘ ┴ └┘ └─┘
src └───┘ └────────┘ ┴ └─┘
typ └┘ └┘ └┘ └┘ └───┘ └────────┘ ┴ └┘ └─┘
doc └──┘ └───┘ └────────┘
143 @[simp] lemma move_left_mk {xl xr xL xR i} : (⟨xl, xr, xL, xR⟩ : pgame).move_left i = xL i := rfl
id └┘ └┘ └┘ └┘ └───┘ └───────┘ ┴ ┴ └┘ ┴ └─┘
src └───┘ └───────┘ ┴ └─┘
typ └┘ └┘ └┘ └┘ └───┘ └───────┘ ┴ ┴ └┘ ┴ └─┘
doc └──┘ └───┘ └───────┘
144 @[simp] lemma right_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).right_moves = xr := rfl
id └┘ └┘ └┘ └┘ └───┘ └─────────┘ ┴ └┘ └─┘
src └───┘ └─────────┘ ┴ └─┘
typ └┘ └┘ └┘ └┘ └───┘ └─────────┘ ┴ └┘ └─┘
doc └──┘ └───┘ └─────────┘
145 @[simp] lemma move_right_mk {xl xr xL xR j} : (⟨xl, xr, xL, xR⟩ : pgame).move_right j = xR j := rfl
id └┘ └┘ └┘ └┘ └───┘ └────────┘ ┴ ┴ └┘ ┴ └─┘
src └───┘ └────────┘ ┴ └─┘
typ └┘ └┘ └┘ └┘ └───┘ └────────┘ ┴ ┴ └┘ ┴ └─┘
doc └──┘ └───┘ └────────┘
146
147 /-- `subsequent p q` says that `p` can be obtained by playing
148 some nonempty sequence of moves from `q`. -/
149 inductive subsequent : pgame → pgame → Prop
id └───┘ └───┘
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
150 | left : Π (x : pgame) (i : x.left_moves), subsequent (x.move_left i) x
id └───┘ ┴└─────────┘ ┴└────────┘ ┴ ┴
src └───┘ └─────────┘ └────────┘
typ └───┘ ┴└─────────┘ ┴└────────┘ ┴ ┴
doc └───┘ └─────────┘ └────────┘
151 | right : Π (x : pgame) (j : x.right_moves), subsequent (x.move_right j) x
id └───┘ ┴└──────────┘ ┴└─────────┘ ┴ ┴
src └───┘ └──────────┘ └─────────┘
typ └───┘ ┴└──────────┘ ┴└─────────┘ ┴ ┴
doc └───┘ └──────────┘ └─────────┘
152 | trans : Π (x y z : pgame), subsequent x y → subsequent y z → subsequent x z
id └───┘ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └───┘
typ └───┘ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └───┘
153
154 theorem wf_subsequent : well_founded subsequent :=
id └──────────┘ └────────┘
src └──────────┘ └────────┘
typ └──────────┘ └────────┘
doc └────────┘
155 ⟨λ x, begin
id ┴
typ ┴
st └─────
156 induction x with l r L R IHl IHr,
id ┴
src └────────┘ └───────────────────┘
typ └────────┘┴└───────────────────┘
doc └────────┘ └───────────────────┘
txt └────────┘ └───────────────────┘
par └────────┘ └───────────────────┘
pid ┴ ┴└──────────────────┘
st ─────────────────────────────────┘└─
157 refine ⟨_, λ y h, _⟩,
src └─────┘ └─┘ └──────┘
typ └─────┘ └─┘ └──────┘
doc └─────┘ └─┘ └──────┘
txt └─────┘ └─┘ └──────┘
par └─────┘ └─┘ └──────┘
pid ┴ └─┘ └──────┘
st ─────────────────────┘└─
158 generalize_hyp e : mk l r L R = x at h,
id └┘ ┴ ┴ ┴ ┴
src └─────────────────┘└┘┴ ┴ ┴ ┴ ┴ ┴ └───┘
typ └─────────────────┘└┘┴┴┴┴┴┴┴┴┴ ┴ └───┘
doc └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
txt └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
par └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
pid └┘└┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
st ───────────────────────────────────────┘└─
159 induction h with _ i _ j a b _ h1 h2 IH1 IH2; subst e,
id ┴ ┴
src └────────┘ └───────────────────────────────┘ └────┘
typ └────────┘┴└───────────────────────────────┘ └────┘┴
doc └────────┘ └───────────────────────────────┘ └────┘
txt └────────┘ └───────────────────────────────┘ └────┘
par └────────┘ └───────────────────────────────┘ └────┘
pid ┴ ┴└──────────────────────────────┘ ┴
st ──────────────────────────────────────────────────────┘└─
160 { apply IHl },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└────────┘└┘└
161 { apply IHr },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└────────┘└┘└
162 { exact acc.inv (IH2 rfl) h1 }
id └─────┘ └─┘ └─┘ └┘
src └────┘└─────┘┴ ┴└─┘└┘ ┴
typ └────┘└─────┘┴ └─┘┴└─┘└┘└┘┴
doc └────┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ──────────────────────────────┘└─
163 end⟩
st ──┘
164
165 instance : has_well_founded pgame :=
id └──────────────┘ └───┘
src └──────────────┘ └───┘
typ └──────────────┘ └───┘
doc └───┘
166 { r := subsequent,
id └────────┘
src └────────┘
typ └────────┘
doc └────────┘
167 wf := wf_subsequent }
id └───────────┘
src └───────────┘
typ └───────────┘
168
169 /-- A move by Left produces a subsequent game. (For use in pgame_wf_tac.) -/
170 lemma subsequent.left_move {xl xr} {xL : xl → pgame} {xR : xr → pgame} {i : xl} :
id └┘ └───┘ └┘ └───┘ └┘
src └───┘ └───┘
typ └┘ └───┘ └┘ └───┘ └┘
doc └───┘ └───┘
171 subsequent (xL i) (mk xl xr xL xR) :=
id └────────┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src └────────┘ └┘
typ └────────┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
doc └────────┘
172 subsequent.left (mk xl xr xL xR) i
id └─────────────┘ └┘ └┘ └┘ └┘ └┘ ┴
src └─────────────┘ └┘
typ └─────────────┘ └┘ └┘ └┘ └┘ └┘ ┴
173 /-- A move by Right produces a subsequent game. (For use in pgame_wf_tac.) -/
174 lemma subsequent.right_move {xl xr} {xL : xl → pgame} {xR : xr → pgame} {j : xr} :
id └┘ └───┘ └┘ └───┘ └┘
src └───┘ └───┘
typ └┘ └───┘ └┘ └───┘ └┘
doc └───┘ └───┘
175 subsequent (xR j) (mk xl xr xL xR) :=
id └────────┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src └────────┘ └┘
typ └────────┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
doc └────────┘
176 subsequent.right (mk xl xr xL xR) j
id └──────────────┘ └┘ └┘ └┘ └┘ └┘ ┴
src └──────────────┘ └┘
typ └──────────────┘ └┘ └┘ └┘ └┘ └┘ ┴
177
178 /-- A local tactic for proving well-foundedness of recursive definitions involving pregames. -/
179 meta def pgame_wf_tac :=
id └──────────┘
typ └──────────┘
180 `[solve_by_elim
src └─────────────
typ └─────────────
doc └─────────────
txt └─────────────
par └─────────────
pid └
181 [psigma.lex.left, psigma.lex.right,
src ──┘ └┘ └─
typ ──┘ └┘ └─
doc ──┘ └┘ └─
txt ──┘ └┘ └─
par ──┘ └┘ └─
pid ─┘┴ └┘ └─
182 subsequent.left_move, subsequent.right_move,
src ──┘ └┘ └─
typ ──┘ └┘ └─
doc ──┘ └┘ └─
txt ──┘ └┘ └─
par ──┘ └┘ └─
pid ──┘ └┘ └─
183 subsequent.left, subsequent.right, subsequent.trans]
src ──┘ └┘ └┘ └─
typ ──┘ └┘ └┘ └─
doc ──┘ └┘ └┘ └─
txt ──┘ └┘ └┘ └─
par ──┘ └┘ └┘ └─
pid ──┘ └┘ └┘ ┴└
184 { max_rep := 6 }]
src ─┘ └─────────────┘
typ ─┘ └─────────────┘
doc ─┘ └─────────────┘
txt ─┘ └─────────────┘
par ─┘ └─────────────┘
pid ─┘ └─────────────┘
185
186 /-- The pre-game `zero` is defined by `0 = { | }`. -/
187 instance : has_zero pgame := ⟨⟨pempty, pempty, pempty.elim, pempty.elim⟩⟩
id └──────┘ └───┘ └────┘ └────┘ └─────────┘ └─────────┘
src └──────┘ └───┘ └────┘ └────┘ └─────────┘ └─────────┘
typ └──────┘ └───┘ └────┘ └────┘ └─────────┘ └─────────┘
doc └───┘ └────┘ └────┘
188
189 @[simp] lemma zero_left_moves : (0 : pgame).left_moves = pempty := rfl
id └───┘ └────────┘ ┴ └────┘ └─┘
src └───┘ └────────┘ ┴ └────┘ └─┘
typ └───┘ └────────┘ ┴ └────┘ └─┘
doc └──┘ └───┘ └────────┘ └────┘
190 @[simp] lemma zero_right_moves : (0 : pgame).right_moves = pempty := rfl
id └───┘ └─────────┘ ┴ └────┘ └─┘
src └───┘ └─────────┘ ┴ └────┘ └─┘
typ └───┘ └─────────┘ ┴ └────┘ └─┘
doc └──┘ └───┘ └─────────┘ └────┘
191
192 instance : inhabited pgame := ⟨0⟩
id └───────┘ └───┘
src └───────┘ └───┘
typ └───────┘ └───┘
doc └───┘
193
194 /-- The pre-game `one` is defined by `1 = { 0 | }`. -/
195 instance : has_one pgame := ⟨⟨punit, pempty, λ _, 0, pempty.elim⟩⟩
id └─────┘ └───┘ └───┘ └────┘ ┴ └─────────┘
src └─────┘ └───┘ └───┘ └────┘ └─────────┘
typ └─────┘ └───┘ └───┘ └────┘ ┴ └─────────┘
doc └───┘ └────┘
196
197 @[simp] lemma one_left_moves : (1 : pgame).left_moves = punit := rfl
id └───┘ └────────┘ ┴ └───┘ └─┘
src └───┘ └────────┘ ┴ └───┘ └─┘
typ └───┘ └────────┘ ┴ └───┘ └─┘
doc └──┘ └───┘ └────────┘
198 @[simp] lemma one_move_left : (1 : pgame).move_left punit.star = 0 := rfl
id └───┘ └───────┘ └────────┘ ┴ └─┘
src └───┘ └───────┘ └────────┘ ┴ └─┘
typ └───┘ └───────┘ └────────┘ ┴ └─┘
doc └──┘ └───┘ └───────┘
199 @[simp] lemma one_right_moves : (1 : pgame).right_moves = pempty := rfl
id └───┘ └─────────┘ ┴ └────┘ └─┘
src └───┘ └─────────┘ ┴ └────┘ └─┘
typ └───┘ └─────────┘ ┴ └────┘ └─┘
doc └──┘ └───┘ └─────────┘ └────┘
200
201 /-- Define simultaneously by mutual induction the `<=` and `<`
202 relation on pre-games. The ZFC definition says that `x = {xL | xR}`
203 is less or equal to `y = {yL | yR}` if `∀ x₁ ∈ xL, x₁ < y`
204 and `∀ y₂ ∈ yR, x < y₂`, where `x < y` is the same as `¬ y <= x`.
205 This is a tricky induction because it only decreases one side at
206 a time, and it also swaps the arguments in the definition of `<`.
207 The solution is to define `x < y` and `x <= y` simultaneously. -/
208 def le_lt : Π (x y : pgame), Prop × Prop
id ┴ └───┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴
doc └───┘
209 | (mk xl xr xL xR) (mk yl yr yL yR) :=
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
210 -- the orderings of the clauses here are carefully chosen so that
211 -- and.left/or.inl refer to moves by Left, and
212 -- and.right/or.inr refer to moves by Right.
213 ((∀ i : xl, (le_lt (xL i) ⟨yl, yr, yL, yR⟩).2) ∧ (∀ j : yr, (le_lt ⟨xl, xr, xL, xR⟩ (yR j)).2),
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
214 (∃ i : yl, (le_lt ⟨xl, xr, xL, xR⟩ (yL i)).1) ∨ (∃ j : xr, (le_lt (xR j) ⟨yl, yr, yL, yR⟩).1))
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
215 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
216
217 instance : has_le pgame := ⟨λ x y, (le_lt x y).1⟩
id └────┘ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └────┘ └───┘ └───┘ ┴
typ └────┘ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───┘ └───┘
218 instance : has_lt pgame := ⟨λ x y, (le_lt x y).2⟩
id └────┘ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └────┘ └───┘ └───┘ ┴
typ └────┘ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───┘ └───┘
219
220 /-- Definition of `x ≤ y` on pre-games built using the constructor. -/
221 @[simp] theorem mk_le_mk {xl xr xL xR yl yr yL yR} :
doc └──┘
222 (⟨xl, xr, xL, xR⟩ : pgame) ≤ ⟨yl, yr, yL, yR⟩ ↔
id └┘ └┘ └┘ └┘ └───┘ ┴ └┘ └┘ └┘ └┘ ┴
src └───┘ ┴ ┴
typ └┘ └┘ └┘ └┘ └───┘ ┴ └┘ └┘ └┘ └┘ ┴
doc └───┘
223 (∀ i, xL i < ⟨yl, yr, yL, yR⟩) ∧
id ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴
src ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴
224 (∀ j, (⟨xl, xr, xL, xR⟩ : pgame) < yR j) := iff.rfl
id ┴ └┘ └┘ └┘ └┘ └───┘ ┴ └┘ ┴ └─────┘
src └───┘ ┴ └─────┘
typ ┴ └┘ └┘ └┘ └┘ └───┘ ┴ └┘ ┴ └─────┘
doc └───┘
225
226 /-- Definition of `x ≤ y` on pre-games, in terms of `<` -/
227 theorem le_def_lt {x y : pgame} : x ≤ y ↔
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘
228 (∀ i : x.left_moves, x.move_left i < y) ∧
id ┴└─────────┘ ┴└────────┘ ┴ ┴ ┴ ┴
src └─────────┘ └────────┘ ┴ ┴
typ ┴└─────────┘ ┴└────────┘ ┴ ┴ ┴ ┴
doc └─────────┘ └────────┘
229 (∀ j : y.right_moves, x < y.move_right j) :=
id ┴└──────────┘ ┴ ┴ ┴└─────────┘ ┴
src └──────────┘ ┴ └─────────┘
typ ┴└──────────┘ ┴ ┴ ┴└─────────┘ ┴
doc └──────────┘ └─────────┘
230 by { cases x, cases y, refl }
id ┴ ┴
src └────┘ └────┘ └───┘
typ └────┘┴ └────┘┴ └───┘
doc └────┘ └────┘ └───┘
txt └────┘ └────┘ └───┘
par └────┘ └────┘ └───┘
pid ┴ ┴ ┴
st └────────┘└───────┘└─────┘└┘
231
232 /-- Definition of `x < y` on pre-games built using the constructor. -/
233 @[simp] theorem mk_lt_mk {xl xr xL xR yl yr yL yR} :
doc └──┘
234 (⟨xl, xr, xL, xR⟩ : pgame) < ⟨yl, yr, yL, yR⟩ ↔
id └┘ └┘ └┘ └┘ └───┘ ┴ └┘ └┘ └┘ └┘ ┴
src └───┘ ┴ ┴
typ └┘ └┘ └┘ └┘ └───┘ ┴ └┘ └┘ └┘ └┘ ┴
doc └───┘
235 (∃ i, (⟨xl, xr, xL, xR⟩ : pgame) ≤ yL i) ∨
id ┴ ┴┴ └┘ └┘ └┘ └┘ └───┘ ┴ └┘ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴┴ └┘ └┘ └┘ └┘ └───┘ ┴ └┘ ┴ ┴
doc └───┘
236 (∃ j, xR j ≤ ⟨yl, yr, yL, yR⟩) := iff.rfl
id ┴ ┴┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └─────┘
src ┴ ┴ ┴ └─────┘
typ ┴ ┴┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └─────┘
237
238 /-- Definition of `x < y` on pre-games, in terms of `≤` -/
239 theorem lt_def_le {x y : pgame} : x < y ↔
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘
240 (∃ i : y.left_moves, x ≤ y.move_left i) ∨
id ┴ ┴└─────────┘┴ ┴ ┴ ┴└────────┘ ┴ ┴
src ┴ └─────────┘┴ ┴ └────────┘ ┴
typ ┴ ┴└─────────┘┴ ┴ ┴ ┴└────────┘ ┴ ┴
doc └─────────┘ └────────┘
241 (∃ j : x.right_moves, x.move_right j ≤ y) :=
id ┴ ┴└──────────┘┴ ┴└─────────┘ ┴ ┴ ┴
src ┴ └──────────┘┴ └─────────┘ ┴
typ ┴ ┴└──────────┘┴ ┴└─────────┘ ┴ ┴ ┴
doc └──────────┘ └─────────┘
242 by { cases x, cases y, refl }
id ┴ ┴
src └────┘ └────┘ └───┘
typ └────┘┴ └────┘┴ └───┘
doc └────┘ └────┘ └───┘
txt └────┘ └────┘ └───┘
par └────┘ └────┘ └───┘
pid ┴ ┴ ┴
st └────────┘└───────┘└─────┘└┘
243
244 /-- The definition of `x ≤ y` on pre-games, in terms of `≤` two moves later. -/
245 theorem le_def {x y : pgame} : x ≤ y ↔
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘
246 (∀ i : x.left_moves,
id ┴└─────────┘
src └─────────┘
typ ┴└─────────┘
doc └─────────┘
247 (∃ i' : y.left_moves, x.move_left i ≤ y.move_left i') ∨
id ┴ ┴└─────────┘┴ ┴└────────┘ ┴ ┴ ┴└────────┘ └┘ ┴
src ┴ └─────────┘┴ └────────┘ ┴ └────────┘ ┴
typ ┴ ┴└─────────┘┴ ┴└────────┘ ┴ ┴ ┴└────────┘ └┘ ┴
doc └─────────┘ └────────┘ └────────┘
248 (∃ j : (x.move_left i).right_moves, (x.move_left i).move_right j ≤ y)) ∧
id ┴ ┴└────────┘ ┴ └─────────┘ ┴ ┴└────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src ┴ └────────┘ └─────────┘ ┴ └────────┘ └────────┘ ┴ ┴
typ ┴ ┴└────────┘ ┴ └─────────┘ ┴ ┴└────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘ └─────────┘ └────────┘ └────────┘
249 (∀ j : y.right_moves,
id ┴└──────────┘
src └──────────┘
typ ┴└──────────┘
doc └──────────┘
250 (∃ i : (y.move_right j).left_moves, x ≤ (y.move_right j).move_left i) ∨
id ┴ ┴└─────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴└─────────┘ ┴ └───────┘ ┴ ┴
src ┴ └─────────┘ └────────┘ ┴ ┴ └─────────┘ └───────┘ ┴
typ ┴ ┴└─────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴└─────────┘ ┴ └───────┘ ┴ ┴
doc └─────────┘ └────────┘ └─────────┘ └───────┘
251 (∃ j' : x.right_moves, x.move_right j' ≤ y.move_right j)) :=
id ┴ ┴└──────────┘┴ ┴└─────────┘ └┘ ┴ ┴└─────────┘ ┴
src ┴ └──────────┘┴ └─────────┘ ┴ └─────────┘
typ ┴ ┴└──────────┘┴ ┴└─────────┘ └┘ ┴ ┴└─────────┘ ┴
doc └──────────┘ └─────────┘ └─────────┘
252 begin
st └─────
253 rw [le_def_lt],
id └───────┘
src └──┘└───────┘┴
typ └──┘└───────┘┴
doc └──┘└───────┘┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ──────────────┘└──
254 conv { to_lhs, simp only [lt_def_le] },
id └───────┘
src └─────┘└────┘└┘└─────────┘└───────┘└┘┴
typ └─────┘└────┘└┘└─────────┘└───────┘└┘┴
doc └───────┘
txt └─────┘└────┘└┘└─────────┘ └┘┴
par └─────┘└────┘└┘└─────────┘ └┘┴
pid ┴└───────────────────┘ └─┘
st ───────┘└─────┘└──────────────────────┘└┘└
255 end
st ──┘
256
257 /-- The definition of `x < y` on pre-games, in terms of `<` two moves later. -/
258 theorem lt_def {x y : pgame} : x < y ↔
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘
259 (∃ i : y.left_moves,
id ┴ ┴└─────────┘┴
src ┴ └─────────┘┴
typ ┴ ┴└─────────┘┴
doc └─────────┘
260 (∀ i' : x.left_moves, x.move_left i' < y.move_left i) ∧
id ┴└─────────┘ ┴└────────┘ └┘ ┴ ┴└────────┘ ┴ ┴
src └─────────┘ └────────┘ ┴ └────────┘ ┴
typ ┴└─────────┘ ┴└────────┘ └┘ ┴ ┴└────────┘ ┴ ┴
doc └─────────┘ └────────┘ └────────┘
261 (∀ j : (y.move_left i).right_moves, x < (y.move_left i).move_right j)) ∨
id ┴└────────┘ ┴ └─────────┘ ┴ ┴ ┴└────────┘ ┴ └────────┘ ┴ ┴
src └────────┘ └─────────┘ ┴ └────────┘ └────────┘ ┴
typ ┴└────────┘ ┴ └─────────┘ ┴ ┴ ┴└────────┘ ┴ └────────┘ ┴ ┴
doc └────────┘ └─────────┘ └────────┘ └────────┘
262 (∃ j : x.right_moves,
id ┴ ┴└──────────┘┴
src ┴ └──────────┘┴
typ ┴ ┴└──────────┘┴
doc └──────────┘
263 (∀ i : (x.move_right j).left_moves, (x.move_right j).move_left i < y) ∧
id ┴└─────────┘ ┴ └────────┘ ┴└─────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴
src └─────────┘ └────────┘ └─────────┘ └───────┘ ┴ ┴
typ ┴└─────────┘ ┴ └────────┘ ┴└─────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └─────────┘ └────────┘ └─────────┘ └───────┘
264 (∀ j' : y.right_moves, x.move_right j < y.move_right j')) :=
id ┴└──────────┘ ┴└─────────┘ ┴ ┴ ┴└─────────┘ └┘
src └──────────┘ └─────────┘ ┴ └─────────┘
typ ┴└──────────┘ ┴└─────────┘ ┴ ┴ ┴└─────────┘ └┘
doc └──────────┘ └─────────┘ └─────────┘
265 begin
st └─────
266 rw [lt_def_le],
id └───────┘
src └──┘└───────┘┴
typ └──┘└───────┘┴
doc └──┘└───────┘┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ──────────────┘└──
267 conv { to_lhs, simp only [le_def_lt] },
id └───────┘
src └─────┘└────┘└┘└─────────┘└───────┘└┘┴
typ └─────┘└────┘└┘└─────────┘└───────┘└┘┴
doc └───────┘
txt └─────┘└────┘└┘└─────────┘ └┘┴
par └─────┘└────┘└┘└─────────┘ └┘┴
pid ┴└───────────────────┘ └─┘
st ───────┘└─────┘└──────────────────────┘└┘└
268 end
st ──┘
269
270 /-- The definition of `x ≤ 0` on pre-games, in terms of `≤ 0` two moves later. -/
271 theorem le_zero {x : pgame} : x ≤ 0 ↔
id └───┘ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴
doc └───┘
272 ∀ i : x.left_moves, ∃ j : (x.move_left i).right_moves, (x.move_left i).move_right j ≤ 0 :=
id ┴└─────────┘ ┴ ┴└────────┘ ┴ └─────────┘ ┴ ┴└────────┘ ┴ └────────┘ ┴ ┴
src └─────────┘ ┴ └────────┘ └─────────┘ ┴ └────────┘ └────────┘ ┴
typ ┴└─────────┘ ┴ ┴└────────┘ ┴ └─────────┘ ┴ ┴└────────┘ ┴ └────────┘ ┴ ┴
doc └─────────┘ └────────┘ └─────────┘ └────────┘ └────────┘
273 begin
st └─────
274 rw le_def,
id └────┘
src └─┘└────┘
typ └─┘└────┘
doc └─┘└────┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
275 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
276 simp [forall_pempty, exists_pempty]
id └───────────┘ └───────────┘
src └────┘└───────────┘└┘└───────────┘└┘
typ └────┘└───────────┘└┘└───────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────────────────┘
277 end
st └─┘
278
279 /-- The definition of `0 ≤ x` on pre-games, in terms of `0 ≤` two moves later. -/
280 theorem zero_le {x : pgame} : 0 ≤ x ↔
id └───┘ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴
doc └───┘
281 ∀ j : x.right_moves, ∃ i : (x.move_right j).left_moves, 0 ≤ (x.move_right j).move_left i :=
id ┴└──────────┘ ┴ ┴└─────────┘ ┴ └────────┘ ┴ ┴ ┴└─────────┘ ┴ └───────┘ ┴
src └──────────┘ ┴ └─────────┘ └────────┘ ┴ ┴ └─────────┘ └───────┘
typ ┴└──────────┘ ┴ ┴└─────────┘ ┴ └────────┘ ┴ ┴ ┴└─────────┘ ┴ └───────┘ ┴
doc └──────────┘ └─────────┘ └────────┘ └─────────┘ └───────┘
282 begin
st └─────
283 rw le_def,
id └────┘
src └─┘└────┘
typ └─┘└────┘
doc └─┘└────┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
284 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
285 simp [forall_pempty, exists_pempty]
id └───────────┘ └───────────┘
src └────┘└───────────┘└┘└───────────┘└┘
typ └────┘└───────────┘└┘└───────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────────────────┘
286 end
st └─┘
287
288 /-- The definition of `x < 0` on pre-games, in terms of `< 0` two moves later. -/
289 theorem lt_zero {x : pgame} : x < 0 ↔
id └───┘ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴
doc └───┘
290 ∃ j : x.right_moves, ∀ i : (x.move_right j).left_moves, (x.move_right j).move_left i < 0 :=
id ┴ ┴└──────────┘┴ ┴└─────────┘ ┴ └────────┘ ┴└─────────┘ ┴ └───────┘ ┴ ┴
src ┴ └──────────┘┴ └─────────┘ └────────┘ └─────────┘ └───────┘ ┴
typ ┴ ┴└──────────┘┴ ┴└─────────┘ ┴ └────────┘ ┴└─────────┘ ┴ └───────┘ ┴ ┴
doc └──────────┘ └─────────┘ └────────┘ └─────────┘ └───────┘
291 begin
st └─────
292 rw lt_def,
id └────┘
src └─┘└────┘
typ └─┘└────┘
doc └─┘└────┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
293 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
294 simp [forall_pempty, exists_pempty]
id └───────────┘ └───────────┘
src └────┘└───────────┘└┘└───────────┘└┘
typ └────┘└───────────┘└┘└───────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────────────────┘
295 end
st └─┘
296
297 /-- The definition of `0 < x` on pre-games, in terms of `< x` two moves later. -/
298 theorem zero_lt {x : pgame} : 0 < x ↔
id └───┘ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴
doc └───┘
299 ∃ i : x.left_moves, ∀ j : (x.move_left i).right_moves, 0 < (x.move_left i).move_right j :=
id ┴ ┴└─────────┘┴ ┴└────────┘ ┴ └─────────┘ ┴ ┴└────────┘ ┴ └────────┘ ┴
src ┴ └─────────┘┴ └────────┘ └─────────┘ ┴ └────────┘ └────────┘
typ ┴ ┴└─────────┘┴ ┴└────────┘ ┴ └─────────┘ ┴ ┴└────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘ └─────────┘ └────────┘ └────────┘
300 begin
st └─────
301 rw lt_def,
id └────┘
src └─┘└────┘
typ └─┘└────┘
doc └─┘└────┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
302 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
303 simp [forall_pempty, exists_pempty]
id └───────────┘ └───────────┘
src └────┘└───────────┘└┘└───────────┘└┘
typ └────┘└───────────┘└┘└───────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────────────────┘
304 end
st └─┘
305
306 /-- Given a right-player-wins game, provide a response to any move by left. -/
307 noncomputable def right_response {x : pgame} (h : x ≤ 0) (i : x.left_moves) :
id └───┘ ┴ ┴ ┴└─────────┘
src └───┘ ┴ └─────────┘
typ └───┘ ┴ ┴ ┴└─────────┘
doc └───┘ └─────────┘
308 (x.move_left i).right_moves :=
id ┴└────────┘ ┴ └─────────┘
src └────────┘ └─────────┘
typ ┴└────────┘ ┴ └─────────┘
doc └────────┘ └─────────┘
309 classical.some $ (le_zero.1 h) i
id └────────────┘ └─────┘┴ ┴ ┴
src └────────────┘ └─────┘┴
typ └────────────┘ └─────┘┴ ┴ ┴
doc └─────┘
310
311 /-- Show that the response for right provided by `right_response`
312 preserves the right-player-wins condition. -/
313 lemma right_response_spec {x : pgame} (h : x ≤ 0) (i : x.left_moves) :
id └───┘ ┴ ┴ ┴└─────────┘
src └───┘ ┴ └─────────┘
typ └───┘ ┴ ┴ ┴└─────────┘
doc └───┘ └─────────┘
314 (x.move_left i).move_right (right_response h i) ≤ 0 :=
id ┴└────────┘ ┴ └────────┘ └────────────┘ ┴ ┴ ┴
src └────────┘ └────────┘ └────────────┘ ┴
typ ┴└────────┘ ┴ └────────┘ └────────────┘ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────────┘
315 classical.some_spec $ (le_zero.1 h) i
id └─────────────────┘ └─────┘┴ ┴ ┴
src └─────────────────┘ └─────┘┴
typ └─────────────────┘ └─────┘┴ ┴ ┴
doc └─────┘
316
317 /-- Given a left-player-wins game, provide a response to any move by right. -/
318 noncomputable def left_response {x : pgame} (h : 0 ≤ x) (j : x.right_moves) :
id └───┘ ┴ ┴ ┴└──────────┘
src └───┘ ┴ └──────────┘
typ └───┘ ┴ ┴ ┴└──────────┘
doc └───┘ └──────────┘
319 (x.move_right j).left_moves :=
id ┴└─────────┘ ┴ └────────┘
src └─────────┘ └────────┘
typ ┴└─────────┘ ┴ └────────┘
doc └─────────┘ └────────┘
320 classical.some $ (zero_le.1 h) j
id └────────────┘ └─────┘┴ ┴ ┴
src └────────────┘ └─────┘┴
typ └────────────┘ └─────┘┴ ┴ ┴
doc └─────┘
321
322 /-- Show that the response for left provided by `left_response`
323 preserves the left-player-wins condition. -/
324 lemma left_response_spec {x : pgame} (h : 0 ≤ x) (j : x.right_moves) :
id └───┘ ┴ ┴ ┴└──────────┘
src └───┘ ┴ └──────────┘
typ └───┘ ┴ ┴ ┴└──────────┘
doc └───┘ └──────────┘
325 0 ≤ (x.move_right j).move_left (left_response h j) :=
id ┴ ┴└─────────┘ ┴ └───────┘ └───────────┘ ┴ ┴
src ┴ └─────────┘ └───────┘ └───────────┘
typ ┴ ┴└─────────┘ ┴ └───────┘ └───────────┘ ┴ ┴
doc └─────────┘ └───────┘ └───────────┘
326 classical.some_spec $ (zero_le.1 h) j
id └─────────────────┘ └─────┘┴ ┴ ┴
src └─────────────────┘ └─────┘┴
typ └─────────────────┘ └─────┘┴ ┴ ┴
doc └─────┘
327
328 theorem lt_of_le_mk {xl xr xL xR y i} :
329 (⟨xl, xr, xL, xR⟩ : pgame) ≤ y → xL i < y :=
id └┘ └┘ └┘ └┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └┘ └┘ └┘ └┘ └───┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───┘
330 by cases y; exact λ h, h.1 i
id ┴ ┴
src └────┘ └────┘ └──┘ └─┘ └
typ └────┘┴ └────┘ └──┘ └─┘┴└
doc └────┘ └────┘ └──┘ └─┘ └
txt └────┘ └────┘ └──┘ └─┘ └
par └────┘ └────┘ └──┘ └─┘ └
pid ┴ ┴ └──┘ └─┘ └
st └──────────────────────────
331
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
332 theorem lt_of_mk_le {x : pgame} {yl yr yL yR i} :
id └───┘
src └───┘
typ └───┘
doc └───┘
333 x ≤ ⟨yl, yr, yL, yR⟩ → x < yR i :=
id ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴
src ┴ ┴
typ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴
334 by cases x; exact λ h, h.2 i
id ┴ ┴
src └────┘ └────┘ └──┘ └─┘ └
typ └────┘┴ └────┘ └──┘ └─┘┴└
doc └────┘ └────┘ └──┘ └─┘ └
txt └────┘ └────┘ └──┘ └─┘ └
par └────┘ └────┘ └──┘ └─┘ └
pid ┴ ┴ └──┘ └─┘ └
st └──────────────────────────
335
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
336 theorem mk_lt_of_le {xl xr xL xR y i} :
337 (by exact xR i ≤ y) → (⟨xl, xr, xL, xR⟩ : pgame) < y :=
id └┘ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └───┘ ┴ ┴
src └────┘ ┴ ┴┴┴ └───┘ ┴
typ └────┘└┘┴┴┴┴┴┴ └┘ └┘ └┘ └┘ └───┘ ┴ ┴
doc └────┘ ┴ ┴ ┴ └───┘
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st └─────────────┘
338 by cases y; exact λ h, or.inr ⟨i, h⟩
id ┴ └────┘ ┴
src └────┘ └────┘ └──┘└────┘┴ └┘ └─
typ └────┘┴ └────┘ └──┘└────┘┴ ┴└┘ └─
doc └────┘ └────┘ └──┘ ┴ └┘ └─
txt └────┘ └────┘ └──┘ ┴ └┘ └─
par └────┘ └────┘ └──┘ ┴ └┘ └─
pid ┴ ┴ └──┘ ┴ └┘ ┴└
st └──────────────────────────────────
339
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
340 theorem lt_mk_of_le {x : pgame} {yl yr yL yR i} :
id └───┘
src └───┘
typ └───┘
doc └───┘
341 (by exact x ≤ yL i) → x < ⟨yl, yr, yL, yR⟩ :=
id ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ └┘ └┘
src └────┘ ┴┴┴ ┴ ┴
typ └────┘┴┴┴┴└┘┴┴ ┴ ┴ └┘ └┘ └┘ └┘
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st └─────────────┘
342 by cases x; exact λ h, or.inl ⟨i, h⟩
id ┴ └────┘ ┴
src └────┘ └────┘ └──┘└────┘┴ └┘ └─
typ └────┘┴ └────┘ └──┘└────┘┴ ┴└┘ └─
doc └────┘ └────┘ └──┘ ┴ └┘ └─
txt └────┘ └────┘ └──┘ ┴ └┘ └─
par └────┘ └────┘ └──┘ ┴ └┘ └─
pid ┴ ┴ └──┘ ┴ └┘ ┴└
st └──────────────────────────────────
343
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
344 theorem not_le_lt {x y : pgame} :
id └───┘
src └───┘
typ └───┘
doc └───┘
345 (¬ x ≤ y ↔ y < x) ∧ (¬ x < y ↔ y ≤ x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
346 begin
st └─────
347 induction x with xl xr xL xR IHxl IHxr generalizing y,
id ┴
src └────────┘ └────────────────────────────────────────┘
typ └────────┘┴└────────────────────────────────────────┘
doc └────────┘ └────────────────────────────────────────┘
txt └────────┘ └────────────────────────────────────────┘
par └────────┘ └────────────────────────────────────────┘
pid ┴ ┴└────────────────────────┘└─────────────┘
st ──────────────────────────────────────────────────────┘└─
348 induction y with yl yr yL yR IHyl IHyr,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└────────────────────────┘
st ───────────────────────────────────────┘└─
349 classical,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────┘└─
350 simp only [mk_le_mk, mk_lt_mk,
id └──────┘ └──────┘
src └─────────┘└──────┘└┘└──────┘└─
typ └─────────┘└──────┘└┘└──────┘└─
doc └─────────┘└──────┘└┘└──────┘└─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ └─
st ─────────────────────────────────
351 not_and_distrib, not_or_distrib, not_forall, not_exists,
id └─────────────┘ └────────────┘ └────────┘ └────────┘
src ───┘└─────────────┘└┘└────────────┘└┘└────────┘└┘└────────┘└─
typ ───┘└─────────────┘└┘└────────────┘└┘└────────┘└┘└────────┘└─
doc ───┘ └┘ └┘ └┘ └─
txt ───┘ └┘ └┘ └┘ └─
par ───┘ └┘ └┘ └┘ └─
pid ───┘ └┘ └┘ └┘ └─
st ─────────────────────────────────────────────────────────────
352 and_comm, or_comm, IHxl, IHxr, IHyl, IHyr, iff_self, and_self]
id └──────┘ └─────┘ └──┘ └──┘ └──┘ └──┘ └──────┘ └──────┘
src ───┘└──────┘└┘└─────┘└┘ └┘ └┘ └┘ └┘└──────┘└┘└──────┘└┘
typ ───┘└──────┘└┘└─────┘└┘└──┘└┘└──┘└┘└──┘└┘└──┘└┘└──────┘└┘└──────┘└┘
doc ───┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
txt ───┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
par ───┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
pid ───┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴
st ──────────────────────────────────────────────────────────────────┘
353 end
st └─┘
354
355 theorem not_le {x y : pgame} : ¬ x ≤ y ↔ y < x := not_le_lt.1
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘┴
src └───┘ ┴ ┴ ┴ ┴ └───────┘┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘┴
doc └───┘
356 theorem not_lt {x y : pgame} : ¬ x < y ↔ y ≤ x := not_le_lt.2
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘┴
src └───┘ ┴ ┴ ┴ ┴ └───────┘┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘┴
doc └───┘
357
358 @[refl] theorem le_refl : ∀ x : pgame, x ≤ x
id ┴ └───┘ ┴ ┴ ┴
src └──┘ ┴ └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴
doc └──┘ └───┘
359 | ⟨l, r, L, R⟩ :=
360 ⟨λ i, lt_mk_of_le (le_refl _), λ i, mk_lt_of_le (le_refl _)⟩
id ┴ └─────────┘ └─────┘ ┴ └─────────┘ └─────┘
src └─────────┘ └─────┘ └─────────┘ └─────┘
typ ┴ └─────────┘ └─────┘ ┴ └─────────┘ └─────┘
361
362 theorem lt_irrefl (x : pgame) : ¬ x < x :=
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘
363 not_lt.2 (le_refl _)
id └────┘┴ └─────┘
src └────┘┴ └─────┘
typ └────┘┴ └─────┘
364
365 theorem ne_of_lt : ∀ {x y : pgame}, x < y → x ≠ y
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
366 | x _ h rfl := lt_irrefl x h
id ┴ ┴ └─┘ └───────┘
src └─┘ └───────┘
typ ┴ ┴ └─┘ └───────┘
367
368 theorem le_trans_aux
369 {xl xr} {xL : xl → pgame} {xR : xr → pgame}
id └┘ └───┘ └┘ └───┘
src └───┘ └───┘
typ └┘ └───┘ └┘ └───┘
doc └───┘ └───┘
370 {yl yr} {yL : yl → pgame} {yR : yr → pgame}
id └┘ └───┘ └┘ └───┘
src └───┘ └───┘
typ └┘ └───┘ └┘ └───┘
doc └───┘ └───┘
371 {zl zr} {zL : zl → pgame} {zR : zr → pgame}
id └┘ └───┘ └┘ └───┘
src └───┘ └───┘
typ └┘ └───┘ └┘ └───┘
doc └───┘ └───┘
372 (h₁ : ∀ i, mk yl yr yL yR ≤ mk zl zr zL zR → mk zl zr zL zR ≤ xL i → mk yl yr yL yR ≤ xL i)
id ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴
src └┘ ┴ └┘ └┘ ┴ └┘ ┴
typ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴
373 (h₂ : ∀ i, zR i ≤ mk xl xr xL xR → mk xl xr xL xR ≤ mk yl yr yL yR → zR i ≤ mk yl yr yL yR) :
id ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘
src ┴ └┘ └┘ ┴ └┘ ┴ └┘
typ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘
374 mk xl xr xL xR ≤ mk yl yr yL yR →
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src └┘ ┴ └┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
375 mk yl yr yL yR ≤ mk zl zr zL zR →
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src └┘ ┴ └┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
376 mk xl xr xL xR ≤ mk zl zr zL zR :=
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src └┘ ┴ └┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
377 λ ⟨xLy, xyR⟩ ⟨yLz, yzR⟩, ⟨
id ┴└─┘ └─┘ ┴└─┘ └─┘
typ ┴└─┘ └─┘ ┴└─┘ └─┘
378 λ i, not_le.1 (λ h, not_lt.2 (h₁ _ ⟨yLz, yzR⟩ h) (xLy _)),
id ┴ └────┘┴ ┴ └────┘┴ └┘ ┴
src └────┘┴ └────┘┴
typ ┴ └────┘┴ ┴ └────┘┴ └┘ ┴
379 λ i, not_le.1 (λ h, not_lt.2 (h₂ _ h ⟨xLy, xyR⟩) (yzR _))⟩
id ┴ └────┘┴ ┴ └────┘┴ └┘ ┴
src └────┘┴ └────┘┴
typ ┴ └────┘┴ ┴ └────┘┴ └┘ ┴
380
381 @[trans] theorem le_trans {x y z : pgame} : x ≤ y → y ≤ z → x ≤ z :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
382 suffices ∀ {x y z : pgame},
id └───┘
src └───┘
typ └───┘
doc └───┘
383 (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
384 from this.1, begin
id └──┘┴
src ┴
typ └──┘┴
st └─────
385 clear x y z, intros,
src └─────────┘ └────┘
typ └─────────┘ └────┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid └────┘
st ────────────┘└──────┘└─
386 induction x with xl xr xL xR IHxl IHxr generalizing y z,
id ┴
src └────────┘ └──────────────────────────────────────────┘
typ └────────┘┴└──────────────────────────────────────────┘
doc └────────┘ └──────────────────────────────────────────┘
txt └────────┘ └──────────────────────────────────────────┘
par └────────┘ └──────────────────────────────────────────┘
pid ┴ ┴└────────────────────────┘└───────────────┘
st ────────────────────────────────────────────────────────┘└─
387 induction y with yl yr yL yR IHyl IHyr generalizing z,
id ┴
src └────────┘ └────────────────────────────────────────┘
typ └────────┘┴└────────────────────────────────────────┘
doc └────────┘ └────────────────────────────────────────┘
txt └────────┘ └────────────────────────────────────────┘
par └────────┘ └────────────────────────────────────────┘
pid ┴ ┴└────────────────────────┘└─────────────┘
st ──────────────────────────────────────────────────────┘└─
388 induction z with zl zr zL zR IHzl IHzr,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└────────────────────────┘
st ───────────────────────────────────────┘└─
389 exact ⟨
src └────┘ └
typ └────┘ └
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ──────────
390 le_trans_aux (λ i, (IHxl _).2.1) (λ i, (IHzr _).2.2),
id └──┘ └──┘
src ───┘ ┴ └──┘ └───────┘ └──┘ └─────────
typ ───┘ ┴ └──┘ └──┘└───────┘ └──┘ └──┘└─────────
doc ───┘ ┴ └──┘ └───────┘ └──┘ └─────────
txt ───┘ ┴ └──┘ └───────┘ └──┘ └─────────
par ───┘ ┴ └──┘ └───────┘ └──┘ └─────────
pid ───┘ ┴ └──┘ └───────┘ └──┘ └─────────
st ──────────────────────────────────────────────────────────
391 le_trans_aux (λ i, (IHyl _).2.2) (λ i, (IHxr _).1),
id └──┘ └──┘
src ───┘ ┴ └──┘ └───────┘ └──┘ └───────
typ ───┘ ┴ └──┘ └──┘└───────┘ └──┘ └──┘└───────
doc ───┘ ┴ └──┘ └───────┘ └──┘ └───────
txt ───┘ ┴ └──┘ └───────┘ └──┘ └───────
par ───┘ ┴ └──┘ └───────┘ └──┘ └───────
pid ───┘ ┴ └──┘ └───────┘ └──┘ └───────
st ────────────────────────────────────────────────────────
392 le_trans_aux (λ i, (IHzl _).1) (λ i, (IHyr _).2.1)⟩,
id └──────────┘ └──┘ └──┘
src ───┘└──────────┘┴ └──┘ └─────┘ └──┘ └───────┘
typ ───┘└──────────┘┴ └──┘ └──┘└─────┘ └──┘ └──┘└───────┘
doc ───┘ ┴ └──┘ └─────┘ └──┘ └───────┘
txt ───┘ ┴ └──┘ └─────┘ └──┘ └───────┘
par ───┘ ┴ └──┘ └─────┘ └──┘ └───────┘
pid ───┘ ┴ └──┘ └─────┘ └──┘ └───────┘
st ──────────────────────────────────────────────────────┘└─
393 end
st ──┘
394
395 @[trans] theorem lt_of_le_of_lt {x y z : pgame} (hxy : x ≤ y) (hyz : y < z) : x < z :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
396 begin
st └─────
397 rw ←not_le at ⊢ hyz,
id └────┘
src └──┘└────┘└───────┘
typ └──┘└────┘└───────┘
doc └──┘ └───────┘
txt └──┘ └───────┘
par └──┘ └───────┘
pid └┘ └───────┘
st ────────────────────┘└─
398 exact mt (λ H, le_trans H hxy) hyz
id └┘ └──────┘ └─┘ └─┘
src └────┘└┘┴ └──┘└──────┘┴ ┴ └┘ ┴
typ └────┘└┘┴ └──┘└──────┘┴ ┴└─┘└┘└─┘┴
doc └────┘ ┴ └──┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ └──┘ ┴ ┴ └┘ ┴
par └────┘ ┴ └──┘ ┴ ┴ └┘ ┴
pid ┴ ┴ └──┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────┘
399 end
st └─┘
400
401 @[trans] theorem lt_of_lt_of_le {x y z : pgame} (hxy : x < y) (hyz : y ≤ z) : x < z :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
402 begin
st └─────
403 rw ←not_le at ⊢ hxy,
id └────┘
src └──┘└────┘└───────┘
typ └──┘└────┘└───────┘
doc └──┘ └───────┘
txt └──┘ └───────┘
par └──┘ └───────┘
pid └┘ └───────┘
st ────────────────────┘└─
404 exact mt (λ H, le_trans hyz H) hxy
id └┘ └──────┘ └─┘ └─┘
src └────┘└┘┴ └──┘└──────┘┴ ┴ └┘ ┴
typ └────┘└┘┴ └──┘└──────┘┴└─┘┴ └┘└─┘┴
doc └────┘ ┴ └──┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ └──┘ ┴ ┴ └┘ ┴
par └────┘ ┴ └──┘ ┴ ┴ └┘ ┴
pid ┴ ┴ └──┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────┘
405 end
st └─┘
406
407 /-- Define the equivalence relation on pre-games. Two pre-games
408 `x`, `y` are equivalent if `x ≤ y` and `y ≤ x`. -/
409 def equiv (x y : pgame) : Prop := x ≤ y ∧ y ≤ x
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
410
411 local infix ` ≈ ` := pgame.equiv
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
412
413 @[refl] theorem equiv_refl (x) : x ≈ x := ⟨le_refl _, le_refl _⟩
id ┴ ┴ ┴ └─────┘ └─────┘
src └──┘ ┴ └─────┘ └─────┘
typ ┴ ┴ ┴ └─────┘ └─────┘
doc └──┘ ┴
414 @[symm] theorem equiv_symm {x y} : x ≈ y → y ≈ x | ⟨xy, yx⟩ := ⟨yx, xy⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
src └──┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
doc └──┘ ┴ ┴
415 @[trans] theorem equiv_trans {x y z} : x ≈ y → y ≈ z → x ≈ z
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴ ┴ ┴
416 | ⟨xy, yx⟩ ⟨yz, zy⟩ := ⟨le_trans xy yz, le_trans zy yx⟩
id └┘ └┘ └┘ └┘ └──────┘ └──────┘
src └──────┘ └──────┘
typ └┘ └┘ └┘ └┘ └──────┘ └──────┘
417
418 theorem lt_of_lt_of_equiv {x y z} (h₁ : x < y) (h₂ : y ≈ z) : x < z := lt_of_lt_of_le h₁ h₂.1
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘ └┘┴
src ┴ ┴ ┴ └────────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘ └┘┴
doc ┴
419 theorem le_of_le_of_equiv {x y z} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z := le_trans h₁ h₂.1
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘ └┘┴
src ┴ ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘ └┘┴
doc ┴
420 theorem lt_of_equiv_of_lt {x y z} (h₁ : x ≈ y) (h₂ : y < z) : x < z := lt_of_le_of_lt h₁.1 h₂
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘┴ └┘
src ┴ ┴ ┴ └────────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘┴ └┘
doc ┴
421 theorem le_of_equiv_of_le {x y z} (h₁ : x ≈ y) (h₂ : y ≤ z) : x ≤ z := le_trans h₁.1 h₂
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘┴ └┘
src ┴ ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘┴ └┘
doc ┴
422
423 theorem le_congr {x₁ y₁ x₂ y₂} : x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ≤ y₁ ↔ x₂ ≤ y₂)
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
doc ┴ ┴
424 | ⟨x12, x21⟩ ⟨y12, y21⟩ := ⟨λ h, le_trans x21 (le_trans h y12), λ h, le_trans x12 (le_trans h y21)⟩
id └─┘ └─┘ └─┘ └─┘ ┴ └──────┘ └──────┘ ┴ ┴ └──────┘ └──────┘ ┴
src └──────┘ └──────┘ └──────┘ └──────┘
typ └─┘ └─┘ └─┘ └─┘ ┴ └──────┘ └──────┘ ┴ ┴ └──────┘ └──────┘ ┴
425
426 theorem lt_congr {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ < y₁ ↔ x₂ < y₂ :=
id └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
doc ┴ ┴
427 not_le.symm.trans $ (not_congr (le_congr hy hx)).trans not_le
id └────┘└───┘└────┘ └───────┘ └──────┘ └┘ └┘ └───┘ └────┘
src └────┘└───┘└────┘ └───────┘ └──────┘ └───┘ └────┘
typ └────┘└───┘└────┘ └───────┘ └──────┘ └┘ └┘ └───┘ └────┘
428
429 /-- `restricted x y` says that Left always has no more moves in `x` than in `y`,
430 and Right always has no more moves in `y` than in `x` -/
431 inductive restricted : pgame.{u} → pgame.{u} → Type (u+1)
id └───┘ └───┘
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
432 | mk : Π {x y : pgame} (L : x.left_moves → y.left_moves) (R : y.right_moves → x.right_moves),
id └───┘ ┴└─────────┘ ┴ ┴└─────────┘ ┴└──────────┘ ┴ ┴└──────────┘
src └───┘ └─────────┘ └─────────┘ └──────────┘ └──────────┘
typ └───┘ ┴└─────────┘ ┴ ┴└─────────┘ ┴└──────────┘ ┴ ┴└──────────┘
doc └───┘ └─────────┘ └─────────┘ └──────────┘ └──────────┘
433 (∀ (i : x.left_moves), restricted (x.move_left i) (y.move_left (L i))) →
id ┴ ┴└─────────┘ ┴└────────┘ ┴ ┴└────────┘ ┴ ┴
src └─────────┘ └────────┘ └────────┘
typ ┴ ┴└─────────┘ ┴└────────┘ ┴ ┴└────────┘ ┴ ┴
doc └─────────┘ └────────┘ └────────┘
434 (∀ (j : y.right_moves), restricted (x.move_right (R j)) (y.move_right j)) → restricted x y
id ┴ ┴└──────────┘ ┴└─────────┘ ┴ ┴ ┴└─────────┘ ┴ ┴ ┴
src └──────────┘ └─────────┘ └─────────┘
typ ┴ ┴└──────────┘ ┴└─────────┘ ┴ ┴ ┴└─────────┘ ┴ ┴ ┴
doc └──────────┘ └─────────┘ └─────────┘
435
436 /-- The identity restriction. -/
437 @[refl] def restricted.refl : Π (x : pgame), restricted x x
id ┴ └───┘ └────────┘ ┴ ┴
src └──┘ └───┘ └────────┘
typ ┴ └───┘ └────────┘ ┴ ┴
doc └──┘ └───┘ └────────┘
438 | (mk xl xr xL xR) :=
id └┘
src └┘
typ └┘
439 restricted.mk
id └───────────┘
src └───────────┘
typ └───────────┘
440 id id
id └┘ └┘
src └┘ └┘
typ └┘ └┘
441 (λ i, restricted.refl _) (λ j, restricted.refl _)
id ┴ └─────────────┘ ┴ └─────────────┘
typ ┴ └─────────────┘ ┴ └─────────────┘
442 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
443
444 -- TODO trans for restricted
445
446 theorem le_of_restricted : Π {x y : pgame} (r : restricted x y), x ≤ y
id ┴ └───┘ └────────┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └────────┘ ┴
typ ┴ └───┘ └────────┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └────────┘
447 | (mk xl xr xL xR) (mk yl yr yL yR)
id └┘
src └┘
typ └┘
448 (restricted.mk L_embedding R_embedding L_restriction R_restriction) :=
id └───────────┘
src └───────────┘
typ └───────────┘
449 begin
st └─────
450 rw le_def,
id └────┘
src └─┘└────┘
typ └─┘└────┘
doc └─┘└────┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
451 exact
src └─────
typ └─────
doc └─────
txt └─────
par └─────
pid └
st ────────
452 ⟨λ i, or.inl ⟨L_embedding i, le_of_restricted (L_restriction i)⟩,
id └────┘ └─────────┘ └───────────┘
src ───┘ └──┘└────┘┴ ┴ └┘ ┴ ┴ └───
typ ───┘ └──┘└────┘┴ └─────────┘┴ └┘ ┴ └───────────┘┴ └───
doc ───┘ └──┘ ┴ ┴ └┘ ┴ ┴ └───
txt ───┘ └──┘ ┴ ┴ └┘ ┴ ┴ └───
par ───┘ └──┘ ┴ ┴ └┘ ┴ ┴ └───
pid ───┘ └──┘ ┴ ┴ └┘ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────────────
453 λ i, or.inr ⟨R_embedding i, le_of_restricted (R_restriction i)⟩⟩
id └────┘ └─────────┘ └──────────────┘ └───────────┘
src ────┘ └──┘└────┘┴ ┴ └┘ ┴ ┴ └──┘
typ ────┘ └──┘└────┘┴ └─────────┘┴ └┘└──────────────┘┴ └───────────┘┴ └──┘
doc ────┘ └──┘ ┴ ┴ └┘ ┴ ┴ └──┘
txt ────┘ └──┘ ┴ ┴ └┘ ┴ ┴ └──┘
par ────┘ └──┘ ┴ ┴ └┘ ┴ ┴ └──┘
pid ────┘ └──┘ ┴ ┴ └┘ ┴ ┴ └─┘┴
st ─────────────────────────────────────────────────────────────────────┘
454 end
st └─┘
455
456 /-- `relabelling x y` says that `x` and `y` are really the same game, just dressed up differently.
457 Specifically, there is a bijection between the moves for Left in `x` and in `y`, and similarly
458 for Right, and under these bijections we inductively have `relabelling`s for the consequent games. -/
459 inductive relabelling : pgame.{u} → pgame.{u} → Type (u+1)
id └───┘ └───┘
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
460 | mk : Π {x y : pgame} (L : x.left_moves ≃ y.left_moves) (R : x.right_moves ≃ y.right_moves),
id └───┘ ┴└─────────┘ ┴ ┴└─────────┘ ┴└──────────┘ ┴ ┴└──────────┘
src └───┘ └─────────┘ ┴ └─────────┘ └──────────┘ ┴ └──────────┘
typ └───┘ ┴└─────────┘ ┴ ┴└─────────┘ ┴└──────────┘ ┴ ┴└──────────┘
doc └───┘ └─────────┘ ┴ └─────────┘ └──────────┘ ┴ └──────────┘
461 (∀ (i : x.left_moves), relabelling (x.move_left i) (y.move_left (L i))) →
id ┴ ┴└─────────┘ ┴└────────┘ ┴ ┴└────────┘ ┴ ┴
src └─────────┘ └────────┘ └────────┘
typ ┴ ┴└─────────┘ ┴└────────┘ ┴ ┴└────────┘ ┴ ┴
doc └─────────┘ └────────┘ └────────┘
462 (∀ (j : y.right_moves), relabelling (x.move_right (R.symm j)) (y.move_right j)) →
id ┴ ┴└──────────┘ ┴└─────────┘ ┴└───┘ ┴ ┴└─────────┘ ┴
src └──────────┘ └─────────┘ └───┘ └─────────┘
typ ┴ ┴└──────────┘ ┴└─────────┘ ┴└───┘ ┴ ┴└─────────┘ ┴
doc └──────────┘ └─────────┘ └─────────┘
463 relabelling x y
id ┴ ┴
typ ┴ ┴
464
465 /-- If `x` is a relabelling of `y`, then Left and Right have the same moves in either game,
466 so `x` is a restriction of `y`. -/
467 def restricted_of_relabelling : Π {x y : pgame} (r : relabelling x y), restricted x y
id ┴ └───┘ └─────────┘ ┴ ┴ └────────┘ ┴ ┴
src └───┘ └─────────┘ └────────┘
typ ┴ └───┘ └─────────┘ ┴ ┴ └────────┘ ┴ ┴
doc └───┘ └─────────┘ └────────┘
468 | (mk xl xr xL xR) (mk yl yr yL yR) (relabelling.mk L_equiv R_equiv L_relabelling R_relabelling) :=
id └┘ └────────────┘ └─────┘ └─────┘ └───────────┘ └───────────┘
src └┘ └────────────┘
typ └┘ └────────────┘ └─────┘ └─────┘ └───────────┘ └───────────┘
469 restricted.mk L_equiv.to_embedding R_equiv.symm.to_embedding
id └───────────┘ └───────────┘ └───┘└───────────┘
src └───────────┘ └───────────┘ └───┘└───────────┘
typ └───────────┘ └───────────┘ └───┘└───────────┘
470 (λ i, restricted_of_relabelling (L_relabelling i))
id ┴ └───────────────────────┘ ┴
typ ┴ └───────────────────────┘ ┴
471 (λ j, restricted_of_relabelling (R_relabelling j))
id ┴ └───────────────────────┘ ┴
typ ┴ └───────────────────────┘ ┴
472
473 -- It's not the case that `restricted x y → restricted y x → relabelling x y`,
474 -- but if we insisted that the maps in a restriction were injective, then one
475 -- could use Schröder-Bernstein for do this.
476
477 /-- The identity relabelling. -/
478 @[refl] def relabelling.refl : Π (x : pgame), relabelling x x
id ┴ └───┘ └─────────┘ ┴ ┴
src └──┘ └───┘ └─────────┘
typ ┴ └───┘ └─────────┘ ┴ ┴
doc └──┘ └───┘ └─────────┘
479 | (mk xl xr xL xR) :=
id └┘
src └┘
typ └┘
480 relabelling.mk (equiv.refl _) (equiv.refl _)
id └────────────┘ └────────┘ └────────┘
src └────────────┘ └────────┘ └────────┘
typ └────────────┘ └────────┘ └────────┘
481 (λ i, relabelling.refl _) (λ j, relabelling.refl _)
id ┴ └──────────────┘ ┴ └──────────────┘
typ ┴ └──────────────┘ ┴ └──────────────┘
482 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
483
484 /-- Reverse a relabelling. -/
485 @[symm] def relabelling.symm : Π {x y : pgame}, relabelling x y → relabelling y x
id ┴ └───┘ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴
src └──┘ └───┘ └─────────┘ └─────────┘
typ ┴ └───┘ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴
doc └──┘ └───┘ └─────────┘ └─────────┘
486 | (mk xl xr xL xR) (mk yl yr yL yR) (relabelling.mk L_equiv R_equiv L_relabelling R_relabelling) :=
id └┘ └────────────┘
src └┘ └────────────┘
typ └┘ └────────────┘
487 begin
st └─────
488 refine relabelling.mk L_equiv.symm R_equiv.symm _ _,
id └────────────┘ └──────────┘ └──────────┘
src └─────┘└────────────┘┴└──────────┘┴└──────────┘└──┘
typ └─────┘└────────────┘┴└──────────┘┴└──────────┘└──┘
doc └─────┘ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ └──┘
par └─────┘ ┴ ┴ └──┘
pid ┴ ┴ ┴ └──┘
st ────────────────────────────────────────────────────┘└─
489 { intro i, simpa using (L_relabelling (L_equiv.symm i)).symm },
id └───────────┘ └──────────┘ ┴
src └─────┘ └──────────┘ ┴ └──────────┘┴ └──────┘
typ └─────┘ └──────────┘ └───────────┘┴ └──────────┘┴┴└──────┘
doc └─────┘ └──────────┘ ┴ ┴ └──────┘
txt └─────┘ └──────────┘ ┴ ┴ └──────┘
par └─────┘ └──────────┘ ┴ ┴ └──────┘
pid └┘ ┴└────┘ ┴ ┴ └────┘└┘
st ───┘└─────┘└──────────────────────────────────────────────────┘└┘└
490 { intro j, simpa using (R_relabelling (R_equiv j)).symm }
id └───────────┘ └─────┘ ┴
src └─────┘ └──────────┘ ┴ ┴ └──────┘
typ └─────┘ └──────────┘ └───────────┘┴ └─────┘┴┴└──────┘
doc └─────┘ └──────────┘ ┴ ┴ └──────┘
txt └─────┘ └──────────┘ ┴ ┴ └──────┘
par └─────┘ └──────────┘ ┴ ┴ └──────┘
pid └┘ ┴└────┘ ┴ ┴ └────┘└┘
st ──────────┘└─────────────────────────────────────────────┘└─
491 end
st ──┘
492
493 -- TODO trans for relabelling?
494
495 theorem le_of_relabelling {x y : pgame} (r : relabelling x y) : x ≤ y :=
id └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────────┘ ┴
typ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └─────────┘
496 le_of_restricted (restricted_of_relabelling r)
id └──────────────┘ └───────────────────────┘ ┴
src └──────────────┘ └───────────────────────┘
typ └──────────────┘ └───────────────────────┘ ┴
doc └───────────────────────┘
497
498 /-- A relabelling lets us prove equivalence of games. -/
499 theorem equiv_of_relabelling {x y : pgame} (r : relabelling x y) : x ≈ y :=
id └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────────┘ ┴
typ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └─────────┘ ┴
500 ⟨le_of_relabelling r, le_of_relabelling r.symm⟩
id └───────────────┘ ┴ └───────────────┘ ┴└───┘
src └───────────────┘ └───────────────┘ └───┘
typ └───────────────┘ ┴ └───────────────┘ ┴└───┘
doc └───┘
501
502 instance {x y : pgame} : has_coe (relabelling x y) (x ≈ y) := ⟨equiv_of_relabelling⟩
id └───┘ └─────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └──────────────────┘
src └───┘ └─────┘ └─────────┘ ┴ └──────────────────┘
typ └───┘ └─────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └──────────────────┘
doc └───┘ └─────────┘ ┴ └──────────────────┘
503
504 /-- Replace the types indexing the next moves for Left and Right by equivalent types. -/
505 def relabel {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') :=
id └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘
src └───┘ └─────────┘ ┴ └──────────┘ ┴
typ └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘
doc └───┘ └─────────┘ ┴ └──────────┘ ┴
506 pgame.mk xl' xr' (λ i, x.move_left (el.symm i)) (λ j, x.move_right (er.symm j))
id └──────┘ └─┘ └─┘ ┴ ┴└────────┘ └┘└───┘ ┴ ┴ ┴└─────────┘ └┘└───┘ ┴
src └──────┘ └────────┘ └───┘ └─────────┘ └───┘
typ └──────┘ └─┘ └─┘ ┴ ┴└────────┘ └┘└───┘ ┴ ┴ ┴└─────────┘ └┘└───┘ ┴
doc └────────┘ └─────────┘
507
508 @[simp] lemma relabel_move_left {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (i : x.left_moves) :
id └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ ┴└─────────┘
src └───┘ └─────────┘ ┴ └──────────┘ ┴ └─────────┘
typ └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ ┴└─────────┘
doc └──┘ └───┘ └─────────┘ ┴ └──────────┘ ┴ └─────────┘
509 move_left (relabel el er) (el i) = x.move_left i :=
id └───────┘ └─────┘ └┘ └┘ └┘ ┴ ┴ ┴└────────┘ ┴
src └───────┘ └─────┘ ┴ └────────┘
typ └───────┘ └─────┘ └┘ └┘ └┘ ┴ ┴ ┴└────────┘ ┴
doc └───────┘ └─────┘ └────────┘
510 by { dsimp [relabel], simp }
id └─────┘
src └─────┘└─────┘┴ └───┘
typ └─────┘└─────┘┴ └───┘
doc └─────┘└─────┘┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴┴ ┴ ┴
st └────────────────┘└─────┘└┘
511 @[simp] lemma relabel_move_left' {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (i : xl') :
id └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ └─┘
src └───┘ └─────────┘ ┴ └──────────┘ ┴
typ └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ └─┘
doc └──┘ └───┘ └─────────┘ ┴ └──────────┘ ┴
512 move_left (relabel el er) i = x.move_left (el.symm i) :=
id └───────┘ └─────┘ └┘ └┘ ┴ ┴ ┴└────────┘ └┘└───┘ ┴
src └───────┘ └─────┘ ┴ └────────┘ └───┘
typ └───────┘ └─────┘ └┘ └┘ ┴ ┴ ┴└────────┘ └┘└───┘ ┴
doc └───────┘ └─────┘ └────────┘
513 rfl
id └─┘
src └─┘
typ └─┘
514
515 @[simp] lemma relabel_move_right {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (j : x.right_moves) :
id └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ ┴└──────────┘
src └───┘ └─────────┘ ┴ └──────────┘ ┴ └──────────┘
typ └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ ┴└──────────┘
doc └──┘ └───┘ └─────────┘ ┴ └──────────┘ ┴ └──────────┘
516 move_right (relabel el er) (er j) = x.move_right j :=
id └────────┘ └─────┘ └┘ └┘ └┘ ┴ ┴ ┴└─────────┘ ┴
src └────────┘ └─────┘ ┴ └─────────┘
typ └────────┘ └─────┘ └┘ └┘ └┘ ┴ ┴ ┴└─────────┘ ┴
doc └────────┘ └─────┘ └─────────┘
517 by { dsimp [relabel], simp }
id └─────┘
src └─────┘└─────┘┴ └───┘
typ └─────┘└─────┘┴ └───┘
doc └─────┘└─────┘┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴┴ ┴ ┴
st └────────────────┘└─────┘└┘
518 @[simp] lemma relabel_move_right' {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (j : xr') :
id └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ └─┘
src └───┘ └─────────┘ ┴ └──────────┘ ┴
typ └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘ └─┘
doc └──┘ └───┘ └─────────┘ ┴ └──────────┘ ┴
519 move_right (relabel el er) j = x.move_right (er.symm j) :=
id └────────┘ └─────┘ └┘ └┘ ┴ ┴ ┴└─────────┘ └┘└───┘ ┴
src └────────┘ └─────┘ ┴ └─────────┘ └───┘
typ └────────┘ └─────┘ └┘ └┘ ┴ ┴ ┴└─────────┘ └┘└───┘ ┴
doc └────────┘ └─────┘ └─────────┘
520 rfl
id └─┘
src └─┘
typ └─┘
521
522 /-- The game obtained by relabelling the next moves is a relabelling of the original game. -/
523 def relabel_relabelling {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') :
id └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘
src └───┘ └─────────┘ ┴ └──────────┘ ┴
typ └───┘ ┴└─────────┘ ┴ └─┘ ┴└──────────┘ ┴ └─┘
doc └───┘ └─────────┘ ┴ └──────────┘ ┴
524 relabelling x (relabel el er) :=
id └─────────┘ ┴ └─────┘ └┘ └┘
src └─────────┘ └─────┘
typ └─────────┘ ┴ └─────┘ └┘ └┘
doc └─────────┘ └─────┘
525 relabelling.mk el er (λ i, by simp) (λ j, by simp)
id └────────────┘ └┘ └┘ ┴ ┴
src └────────────┘ └──┘ └──┘
typ └────────────┘ └┘ └┘ ┴ └──┘ ┴ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
526
527 /-- The negation of `{L | R}` is `{-R | -L}`. -/
528 def neg : pgame → pgame
id └───┘ ┴ └───┘
src └───┘ └───┘
typ └───┘ ┴ └───┘
doc └───┘ └───┘
529 | ⟨l, r, L, R⟩ := ⟨r, l, λ i, neg (R i), λ i, neg (L i)⟩
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
530
531 instance : has_neg pgame := ⟨neg⟩
id └─────┘ └───┘ └─┘
src └─────┘ └───┘ └─┘
typ └─────┘ └───┘ └─┘
doc └───┘ └─┘
532
533 @[simp] lemma neg_def {xl xr xL xR} : -(mk xl xr xL xR) = mk xr xl (λ j, -(xR j)) (λ i, -(xL i)) :=
id ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
src ┴ └┘ ┴ └┘ ┴ ┴
typ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
doc └──┘
534 rfl
id └─┘
src └─┘
typ └─┘
535
536 @[simp] theorem neg_neg : Π {x : pgame}, -(-x) = x
id ┴ └───┘ ┴ ┴┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴┴ ┴ ┴
doc └──┘ └───┘
537 | (mk xl xr xL xR) :=
id └┘
src └┘
typ └┘
538 begin
st └─────
539 dsimp [has_neg.neg, neg],
id └─┘
src └─────┘ └┘└─┘┴
typ └─────┘ └┘└─┘┴
doc └─────┘ └┘└─┘┴
txt └─────┘ └┘ ┴
par └─────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ─────────────────────────┘└─
540 congr; funext i; apply neg_neg
src └───┘ └──────┘ └────┘ ┴
typ └───┘ └──────┘ └────┘ ┴
doc └──────┘ └────┘ ┴
txt └───┘ └──────┘ └────┘ ┴
par └───┘ └──────┘ └────┘ ┴
pid └┘ ┴ ┴
st ────────────────────────────────┘
541 end
st └─┘
542
543 @[simp] theorem neg_zero : -(0 : pgame) = 0 :=
id ┴ └───┘ ┴
src ┴ └───┘ ┴
typ ┴ └───┘ ┴
doc └──┘ └───┘
544 begin
st └─────
545 dsimp [has_zero.zero, has_neg.neg, neg],
id └─┘
src └─────┘ └┘ └┘└─┘┴
typ └─────┘ └┘ └┘└─┘┴
doc └─────┘ └┘ └┘└─┘┴
txt └─────┘ └┘ └┘ ┴
par └─────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ────────────────────────────────────────┘└─
546 congr; funext i; cases i
id ┴
src └───┘ └──────┘ └────┘ ┴
typ └───┘ └──────┘ └────┘┴┴
doc └──────┘ └────┘ ┴
txt └───┘ └──────┘ └────┘ ┴
par └───┘ └──────┘ └────┘ ┴
pid └┘ ┴ ┴
st ──────────────────────────┘
547 end
st └─┘
548
549 /-- An explicit equivalence between the moves for Left in `-x` and the moves for Right in `x`. -/
550 -- This equivalence is useful to avoid having to use `cases` unnecessarily.
551 def left_moves_neg (x : pgame) : (-x).left_moves ≃ x.right_moves :=
id └───┘ ┴┴ └────────┘ ┴ ┴└──────────┘
src └───┘ ┴ └────────┘ ┴ └──────────┘
typ └───┘ ┴┴ └────────┘ ┴ ┴└──────────┘
doc └───┘ └────────┘ ┴ └──────────┘
552 by { cases x, refl }
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
553
554 /-- An explicit equivalence between the moves for Right in `-x` and the moves for Left in `x`. -/
555 def right_moves_neg (x : pgame) : (-x).right_moves ≃ x.left_moves :=
id └───┘ ┴┴ └─────────┘ ┴ ┴└─────────┘
src └───┘ ┴ └─────────┘ ┴ └─────────┘
typ └───┘ ┴┴ └─────────┘ ┴ ┴└─────────┘
doc └───┘ └─────────┘ ┴ └─────────┘
556 by { cases x, refl }
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
557
558 @[simp] lemma move_right_left_moves_neg {x : pgame} (i : left_moves (-x)) :
id └───┘ └────────┘ ┴┴
src └───┘ └────────┘ ┴
typ └───┘ └────────┘ ┴┴
doc └──┘ └───┘ └────────┘
559 move_right x ((left_moves_neg x) i) = -(move_left (-x) i) :=
id └────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ └───────┘ ┴┴ ┴
src └────────┘ └────────────┘ ┴ ┴ └───────┘ ┴
typ └────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ └───────┘ ┴┴ ┴
doc └────────┘ └────────────┘ └───────┘
560 begin
st └─────
561 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────┘└─
562 exact neg_neg.symm
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────┘
563 end
st └─┘
564 @[simp] lemma move_left_right_moves_neg_symm {x : pgame} (i : right_moves x) :
id └───┘ └─────────┘ ┴
src └───┘ └─────────┘
typ └───┘ └─────────┘ ┴
doc └──┘ └───┘ └─────────┘
565 move_left (-x) ((left_moves_neg x).symm i) = -(move_right x i) :=
id └───────┘ ┴┴ └────────────┘ ┴ └──┘ ┴ ┴ ┴ └────────┘ ┴ ┴
src └───────┘ ┴ └────────────┘ └──┘ ┴ ┴ └────────┘
typ └───────┘ ┴┴ └────────────┘ ┴ └──┘ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └───────┘ └────────────┘ └────────┘
566 by { cases x, refl }
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
567 @[simp] lemma move_left_right_moves_neg {x : pgame} (i : right_moves (-x)) :
id └───┘ └─────────┘ ┴┴
src └───┘ └─────────┘ ┴
typ └───┘ └─────────┘ ┴┴
doc └──┘ └───┘ └─────────┘
568 move_left x ((right_moves_neg x) i) = -(move_right (-x) i) :=
id └───────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴
src └───────┘ └─────────────┘ ┴ ┴ └────────┘ ┴
typ └───────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴
doc └───────┘ └─────────────┘ └────────┘
569 begin
st └─────
570 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────┘└─
571 exact neg_neg.symm
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────┘
572 end
st └─┘
573 @[simp] lemma move_right_right_moves_neg_symm {x : pgame} (i : left_moves x) :
id └───┘ └────────┘ ┴
src └───┘ └────────┘
typ └───┘ └────────┘ ┴
doc └──┘ └───┘ └────────┘
574 move_right (-x) ((right_moves_neg x).symm i) = -(move_left x i) :=
id └────────┘ ┴┴ └─────────────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴
src └────────┘ ┴ └─────────────┘ └──┘ ┴ ┴ └───────┘
typ └────────┘ ┴┴ └─────────────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └────────┘ └─────────────┘ └───────┘
575 by { cases x, refl }
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st └────────┘└─────┘└┘
576
577 theorem le_iff_neg_ge : Π {x y : pgame}, x ≤ y ↔ -y ≤ -x
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └───┘
578 | (mk xl xr xL xR) (mk yl yr yL yR) :=
id └┘
src └┘
typ └┘
579 begin
st └─────
580 rw [le_def],
id └────┘
src └──┘└────┘┴
typ └──┘└────┘┴
doc └──┘└────┘┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────┘└──
581 rw [le_def],
id └────┘
src └──┘└────┘┴
typ └──┘└────┘┴
doc └──┘└────┘┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────┘└──
582 dsimp [neg],
id └─┘
src └─────┘└─┘┴
typ └─────┘└─┘┴
doc └─────┘└─┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ────────────┘└─
583 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
584 { intro h,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
585 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
586 { intro i, have t := h.right i, cases t,
id └─────┘ ┴ ┴
src └─────┘ └────────┘└─────┘┴ └────┘
typ └─────┘ └────────┘└─────┘┴┴ └────┘┴
doc └─────┘ └────────┘ ┴ └────┘
txt └─────┘ └────────┘ ┴ └────┘
par └─────┘ └────────┘ ┴ └────┘
pid └┘ └────┘┴└─┘ ┴ ┴
st ─────┘└─────┘└───────────────────┘└───────┘└─
587 { right, cases t, use (@right_moves_neg (yR i)).symm t_w, convert le_iff_neg_ge.1 t_h, simp },
id ┴ └─────────────┘ └┘ ┴ └─┘ └───────────┘ └─┘
src └───┘ └────┘ └──┘ └─────────────┘┴ ┴ └──────┘ └──────┘ └─┘ └───┘
typ └───┘ └────┘┴ └──┘ └─────────────┘┴ └┘┴┴└──────┘└─┘ └──────┘└───────────┘└─┘└─┘ └───┘
doc └───┘ └────┘ └──┘ └─────────────┘┴ ┴ └──────┘ └──────┘ └─┘ └───┘
txt └───┘ └────┘ └──┘ ┴ ┴ └──────┘ └──────┘ └─┘ └───┘
par └───┘ └────┘ └──┘ ┴ ┴ └──────┘ └──────┘ └─┘ └───┘
pid ┴ ┴ ┴ ┴ └──────┘ ┴ └─┘ ┴
st ───────┘└───┘└───────┘└──────────────────────────────────────┘└───────────────────────────┘└─────┘└┘└
588 { left, cases t, use t_w, exact le_iff_neg_ge.1 t_h, } },
id ┴ └─┘ └───────────┘ └─┘
src └──┘ └────┘ └──┘ └────┘ └─┘
typ └──┘ └────┘┴ └──┘└─┘ └────┘└───────────┘└─┘└─┘
doc └──┘ └────┘ └──┘ └────┘ └─┘
txt └──┘ └────┘ └──┘ └────┘ └─┘
par └──┘ └────┘ └──┘ └────┘ └─┘
pid ┴ ┴ ┴ └─┘
st ───────────┘└───────┘└───────┘└─────────────────────────┘└────┘└
589 { intro j, have t := h.left j, cases t,
id └────┘ ┴ ┴
src └─────┘ └────────┘└────┘┴ └────┘
typ └─────┘ └────────┘└────┘┴┴ └────┘┴
doc └─────┘ └────────┘ ┴ └────┘
txt └─────┘ └────────┘ ┴ └────┘
par └─────┘ └────────┘ ┴ └────┘
pid └┘ └────┘┴└─┘ ┴ ┴
st ────────────┘└──────────────────┘└───────┘└─
590 { right, cases t, use t_w, exact le_iff_neg_ge.1 t_h, },
id ┴ └─┘ └───────────┘ └─┘
src └───┘ └────┘ └──┘ └────┘ └─┘
typ └───┘ └────┘┴ └──┘└─┘ └────┘└───────────┘└─┘└─┘
doc └───┘ └────┘ └──┘ └────┘ └─┘
txt └───┘ └────┘ └──┘ └────┘ └─┘
par └───┘ └────┘ └──┘ └────┘ └─┘
pid ┴ ┴ ┴ └─┘
st ───────┘└───┘└───────┘└───────┘└─────────────────────────┘└──┘└
591 { left, cases t, use (@left_moves_neg (xL j)).symm t_w, convert le_iff_neg_ge.1 t_h, simp, } } },
id ┴ └────────────┘ └┘ ┴ └─┘ └───────────┘ └─┘
src └──┘ └────┘ └──┘ └────────────┘┴ ┴ └──────┘ └──────┘ └─┘ └──┘
typ └──┘ └────┘┴ └──┘ └────────────┘┴ └┘┴┴└──────┘└─┘ └──────┘└───────────┘└─┘└─┘ └──┘
doc └──┘ └────┘ └──┘ └────────────┘┴ ┴ └──────┘ └──────┘ └─┘ └──┘
txt └──┘ └────┘ └──┘ ┴ ┴ └──────┘ └──────┘ └─┘ └──┘
par └──┘ └────┘ └──┘ ┴ ┴ └──────┘ └──────┘ └─┘ └──┘
pid ┴ ┴ ┴ ┴ └──────┘ ┴ └─┘
st ───────────┘└───────┘└─────────────────────────────────────┘└───────────────────────────┘└────┘└──────┘└
592 { intro h,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
593 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
594 { intro i, have t := h.right i, cases t,
id └─────┘ ┴ ┴
src └─────┘ └────────┘└─────┘┴ └────┘
typ └─────┘ └────────┘└─────┘┴┴ └────┘┴
doc └─────┘ └────────┘ ┴ └────┘
txt └─────┘ └────────┘ ┴ └────┘
par └─────┘ └────────┘ ┴ └────┘
pid └┘ └────┘┴└─┘ ┴ ┴
st ─────┘└─────┘└───────────────────┘└───────┘└─
595 { right, cases t, use (@left_moves_neg (xL i)) t_w, convert le_iff_neg_ge.2 _, convert t_h, simp, },
id ┴ └────────────┘ └┘ ┴ └─┘ └───────────┘ └─┘
src └───┘ └────┘ └──┘ └────────────┘┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └──┘
typ └───┘ └────┘┴ └──┘ └────────────┘┴ └┘┴┴└─┘└─┘ └──────┘└───────────┘└──┘ └──────┘└─┘ └──┘
doc └───┘ └────┘ └──┘ └────────────┘┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └──┘
txt └───┘ └────┘ └──┘ ┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └──┘
par └───┘ └────┘ └──┘ ┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └──┘
pid ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
st ───────┘└───┘└───────┘└────────────────────────────────┘└─────────────────────────┘└───────────┘└────┘└──┘└
596 { left, cases t, use t_w, exact le_iff_neg_ge.2 t_h, } },
id ┴ └─┘ └───────────┘ └─┘
src └──┘ └────┘ └──┘ └────┘ └─┘
typ └──┘ └────┘┴ └──┘└─┘ └────┘└───────────┘└─┘└─┘
doc └──┘ └────┘ └──┘ └────┘ └─┘
txt └──┘ └────┘ └──┘ └────┘ └─┘
par └──┘ └────┘ └──┘ └────┘ └─┘
pid ┴ ┴ ┴ └─┘
st ───────────┘└───────┘└───────┘└─────────────────────────┘└────┘└
597 { intro j, have t := h.left j, cases t,
id └────┘ ┴ ┴
src └─────┘ └────────┘└────┘┴ └────┘
typ └─────┘ └────────┘└────┘┴┴ └────┘┴
doc └─────┘ └────────┘ ┴ └────┘
txt └─────┘ └────────┘ ┴ └────┘
par └─────┘ └────────┘ ┴ └────┘
pid └┘ └────┘┴└─┘ ┴ ┴
st ────────────┘└──────────────────┘└───────┘└─
598 { right, cases t, use t_w, exact le_iff_neg_ge.2 t_h, },
id ┴ └─┘ └───────────┘ └─┘
src └───┘ └────┘ └──┘ └────┘ └─┘
typ └───┘ └────┘┴ └──┘└─┘ └────┘└───────────┘└─┘└─┘
doc └───┘ └────┘ └──┘ └────┘ └─┘
txt └───┘ └────┘ └──┘ └────┘ └─┘
par └───┘ └────┘ └──┘ └────┘ └─┘
pid ┴ ┴ ┴ └─┘
st ───────┘└───┘└───────┘└───────┘└─────────────────────────┘└──┘└
599 { left, cases t, use (@right_moves_neg (yR j)) t_w, convert le_iff_neg_ge.2 _, convert t_h, simp } } },
id ┴ └─────────────┘ └┘ ┴ └─┘ └───────────┘ └─┘
src └──┘ └────┘ └──┘ └─────────────┘┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └───┘
typ └──┘ └────┘┴ └──┘ └─────────────┘┴ └┘┴┴└─┘└─┘ └──────┘└───────────┘└──┘ └──────┘└─┘ └───┘
doc └──┘ └────┘ └──┘ └─────────────┘┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └───┘
txt └──┘ └────┘ └──┘ ┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └───┘
par └──┘ └────┘ └──┘ ┴ ┴ └─┘ └──────┘ └──┘ └──────┘ └───┘
pid ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴
st ───────────┘└───────┘└─────────────────────────────────┘└─────────────────────────┘└───────────┘└─────┘└──────
600 end
st ──┘
601 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
602
603 theorem neg_congr {x y : pgame} (h : x ≈ y) : -x ≈ -y :=
id └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └───┘ ┴ ┴
604 ⟨le_iff_neg_ge.1 h.2, le_iff_neg_ge.1 h.1⟩
id └───────────┘┴ ┴┴ └───────────┘┴ ┴┴
src └───────────┘┴ ┴ └───────────┘┴ ┴
typ └───────────┘┴ ┴┴ └───────────┘┴ ┴┴
605
606 theorem lt_iff_neg_gt : Π {x y : pgame}, x < y ↔ -y < -x :=
id └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └───┘
607 begin
st └─────
608 classical,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────┘└─
609 intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
610 rw [←not_le, ←not_le, not_iff_not],
id └────┘ └────┘ └─────────┘
src └───┘└────┘└─┘└────┘└┘└─────────┘┴
typ └───┘└────┘└─┘└────┘└┘└─────────┘┴
doc └───┘ └─┘ └┘ ┴
txt └───┘ └─┘ └┘ ┴
par └───┘ └─┘ └┘ ┴
pid └─┘ └─┘ └┘ ┴
st ────────────┘└───────┘└───────────┘└──
611 apply le_iff_neg_ge
id └───────────┘
src └────┘└───────────┘┴
typ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────┘
612 end
st └─┘
613
614 theorem zero_le_iff_neg_le_zero {x : pgame} : 0 ≤ x ↔ -x ≤ 0 :=
id └───┘ ┴ ┴ ┴ ┴┴ ┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴┴ ┴
doc └───┘
615 begin
st └─────
616 convert le_iff_neg_ge,
id └───────────┘
src └──────┘└───────────┘
typ └──────┘└───────────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────────────────┘└─
617 rw neg_zero
id └──────┘
src └─┘└──────┘┴
typ └─┘└──────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────────────┘
618 end
st └─┘
619
620 theorem le_zero_iff_zero_le_neg {x : pgame} : x ≤ 0 ↔ 0 ≤ -x :=
id └───┘ ┴ ┴ ┴ ┴ ┴┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴┴
doc └───┘
621 begin
st └─────
622 convert le_iff_neg_ge,
id └───────────┘
src └──────┘└───────────┘
typ └──────┘└───────────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────────────────┘└─
623 rw neg_zero
id └──────┘
src └─┘└──────┘┴
typ └─┘└──────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────────────┘
624 end
st └─┘
625
626 /-- The sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
627 def add (x y : pgame) : pgame :=
id └───┘ └───┘
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
628 begin
st └─────
629 induction x with xl xr xL xR IHxl IHxr generalizing y,
id ┴
src └────────┘ └────────────────────────────────────────┘
typ └────────┘┴└────────────────────────────────────────┘
doc └────────┘ └────────────────────────────────────────┘
txt └────────┘ └────────────────────────────────────────┘
par └────────┘ └────────────────────────────────────────┘
pid ┴ ┴└────────────────────────┘└─────────────┘
st ──────────────────────────────────────────────────────┘└─
630 induction y with yl yr yL yR IHyl IHyr,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└────────────────────────┘
st ───────────────────────────────────────┘└─
631 have y := mk yl yr yL yR,
id └┘ └┘ └┘ └┘ └┘
src └────────┘└┘┴ ┴ ┴ ┴
typ └────────┘└┘┴└┘┴└┘┴└┘┴└┘
doc └────────┘ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ ┴ ┴
st ─────────────────────────┘└─
632 refine ⟨xl ⊕ yl, xr ⊕ yr, sum.rec _ _, sum.rec _ _⟩,
id └┘ ┴ └┘ └┘ └┘ └─────┘
src └─────┘ ┴┴┴ └┘ ┴ ┴ └┘ └────┘└─────┘└───┘
typ └─────┘ └┘┴┴┴└┘└┘└┘┴ ┴└┘└┘ └────┘└─────┘└───┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ └────┘ └───┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ └────┘ └───┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ └────┘ └───┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘ └────┘ └───┘
st ────────────────────────────────────────────────────┘└─
633 { exact λ i, IHxl i y },
id └──┘ ┴
src └────┘ └──┘ ┴ ┴ ┴
typ └────┘ └──┘└──┘┴ ┴┴┴
doc └────┘ └──┘ ┴ ┴ ┴
txt └────┘ └──┘ ┴ ┴ ┴
par └────┘ └──┘ ┴ ┴ ┴
pid ┴ └──┘ ┴ ┴ ┴
st ───┘└──────────────────┘└┘└
634 { exact λ i, IHyl i },
id └──┘
src └────┘ └──┘ ┴ ┴
typ └────┘ └──┘└──┘┴ ┴
doc └────┘ └──┘ ┴ ┴
txt └────┘ └──┘ ┴ ┴
par └────┘ └──┘ ┴ ┴
pid ┴ └──┘ ┴ ┴
st ───┘└────────────────┘└┘└
635 { exact λ i, IHxr i y },
id └──┘ ┴
src └────┘ └──┘ ┴ ┴ ┴
typ └────┘ └──┘└──┘┴ ┴┴┴
doc └────┘ └──┘ ┴ ┴ ┴
txt └────┘ └──┘ ┴ ┴ ┴
par └────┘ └──┘ ┴ ┴ ┴
pid ┴ └──┘ ┴ ┴ ┴
st ───┘└──────────────────┘└┘└
636 { exact λ i, IHyr i }
id └──┘
src └────┘ └──┘ ┴ ┴
typ └────┘ └──┘└──┘┴ ┴
doc └────┘ └──┘ ┴ ┴
txt └────┘ └──┘ ┴ ┴
par └────┘ └──┘ ┴ ┴
pid ┴ └──┘ ┴ ┴
st ─────────────────────┘└─
637 end
st ──┘
638
639 instance : has_add pgame := ⟨add⟩
id └─────┘ └───┘ └─┘
src └─────┘ └───┘ └─┘
typ └─────┘ └───┘ └─┘
doc └───┘ └─┘
640
641 /-- `x + 0` has exactly the same moves as `x`. -/
642 def add_zero_relabelling : Π (x : pgame.{u}), relabelling (x + 0) x
id ┴ └───┘ └─────────┘ ┴ ┴ ┴
src └───┘ └─────────┘ ┴
typ ┴ └───┘ └─────────┘ ┴ ┴ ┴
doc └───┘ └─────────┘
643 | (mk xl xr xL xR) :=
id └┘
src └┘
typ └┘
644 begin
st └─────
645 refine ⟨equiv.sum_pempty xl, equiv.sum_pempty xr, _, _⟩,
id └┘ └──────────────┘ └┘
src └─────┘ ┴ └┘└──────────────┘┴ └─────┘
typ └─────┘ ┴└┘└┘└──────────────┘┴└┘└─────┘
doc └─────┘ ┴ └┘ ┴ └─────┘
txt └─────┘ ┴ └┘ ┴ └─────┘
par └─────┘ ┴ └┘ ┴ └─────┘
pid ┴ ┴ └┘ ┴ └─────┘
st ────────────────────────────────────────────────────────┘└─
646 { rintro (⟨i⟩|⟨⟨⟩⟩),
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ───┘└───────────────┘└─
647 apply add_zero_relabelling, },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└──┘└
648 { rintro j,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ───────────┘└─
649 apply add_zero_relabelling, }
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└───
650 end
st ──┘
651
652 /-- `x + 0` is equivalent to `x`. -/
653 lemma add_zero_equiv (x : pgame.{u}) : x + 0 ≈ x :=
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘ ┴
654 equiv_of_relabelling (add_zero_relabelling x)
id └──────────────────┘ └──────────────────┘ ┴
src └──────────────────┘ └──────────────────┘
typ └──────────────────┘ └──────────────────┘ ┴
doc └──────────────────┘ └──────────────────┘
655
656 /-- `0 + x` has exactly the same moves as `x`. -/
657 def zero_add_relabelling : Π (x : pgame.{u}), relabelling (0 + x) x
id ┴ └───┘ └─────────┘ ┴ ┴ ┴
src └───┘ └─────────┘ ┴
typ ┴ └───┘ └─────────┘ ┴ ┴ ┴
doc └───┘ └─────────┘
658 | (mk xl xr xL xR) :=
id └┘
src └┘
typ └┘
659 begin
st └─────
660 refine ⟨equiv.pempty_sum xl, equiv.pempty_sum xr, _, _⟩,
id └┘ └──────────────┘ └┘
src └─────┘ ┴ └┘└──────────────┘┴ └─────┘
typ └─────┘ ┴└┘└┘└──────────────┘┴└┘└─────┘
doc └─────┘ ┴ └┘ ┴ └─────┘
txt └─────┘ ┴ └┘ ┴ └─────┘
par └─────┘ ┴ └┘ ┴ └─────┘
pid ┴ ┴ └┘ ┴ └─────┘
st ────────────────────────────────────────────────────────┘└─
661 { rintro (⟨⟨⟩⟩|⟨i⟩),
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ───┘└───────────────┘└─
662 apply zero_add_relabelling, },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└──┘└
663 { rintro j,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ───────────┘└─
664 apply zero_add_relabelling, }
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└───
665 end
st ──┘
666
667 /-- `0 + x` is equivalent to `x`. -/
668 lemma zero_add_equiv (x : pgame.{u}) : 0 + x ≈ x :=
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘ ┴
669 equiv_of_relabelling (zero_add_relabelling x)
id └──────────────────┘ └──────────────────┘ ┴
src └──────────────────┘ └──────────────────┘
typ └──────────────────┘ └──────────────────┘ ┴
doc └──────────────────┘ └──────────────────┘
670
671 /-- An explicit equivalence between the moves for Left in `x + y` and the type-theory sum
672 of the moves for Left in `x` and in `y`. -/
673 def left_moves_add (x y : pgame) : (x + y).left_moves ≃ x.left_moves ⊕ y.left_moves :=
id └───┘ ┴ ┴ ┴ └────────┘ ┴ ┴└─────────┘ ┴ ┴└─────────┘
src └───┘ ┴ └────────┘ ┴ └─────────┘ ┴ └─────────┘
typ └───┘ ┴ ┴ ┴ └────────┘ ┴ ┴└─────────┘ ┴ ┴└─────────┘
doc └───┘ └────────┘ ┴ └─────────┘ └─────────┘
674 by { cases x, cases y, refl, }
id ┴ ┴
src └────┘ └────┘ └──┘
typ └────┘┴ └────┘┴ └──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴
st └────────┘└───────┘└────┘└──┘
675
676 /-- An explicit equivalence between the moves for Right in `x + y` and the type-theory sum
677 of the moves for Right in `x` and in `y`. -/
678 def right_moves_add (x y : pgame) : (x + y).right_moves ≃ x.right_moves ⊕ y.right_moves :=
id └───┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└──────────┘ ┴ ┴└──────────┘
src └───┘ ┴ └─────────┘ ┴ └──────────┘ ┴ └──────────┘
typ └───┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└──────────┘ ┴ ┴└──────────┘
doc └───┘ └─────────┘ ┴ └──────────┘ └──────────┘
679 by { cases x, cases y, refl, }
id ┴ ┴
src └────┘ └────┘ └──┘
typ └────┘┴ └────┘┴ └──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴
st └────────┘└───────┘└────┘└──┘
680
681 @[simp] lemma mk_add_move_left_inl {xl xr yl yr} {xL xR yL yR} {i} :
doc └──┘
682 (mk xl xr xL xR + mk yl yr yL yR).move_left (sum.inl i) = (mk xl xr xL xR).move_left i + (mk yl yr yL yR) :=
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘
src └┘ ┴ └┘ └───────┘ └─────┘ ┴ └┘ └───────┘ ┴ └┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘
doc └───────┘ └───────┘
683 rfl
id └─┘
src └─┘
typ └─┘
684 @[simp] lemma add_move_left_inl {x y : pgame} {i} :
id └───┘
src └───┘
typ └───┘
doc └──┘ └───┘
685 (x + y).move_left ((@left_moves_add x y).symm (sum.inl i)) = x.move_left i + y :=
id ┴ ┴ ┴ └───────┘ └────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴└────────┘ ┴ ┴ ┴
src ┴ └───────┘ └────────────┘ └──┘ └─────┘ ┴ └────────┘ ┴
typ ┴ ┴ ┴ └───────┘ └────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴└────────┘ ┴ ┴ ┴
doc └───────┘ └────────────┘ └────────┘
686 by { cases x, cases y, refl, }
id ┴ ┴
src └────┘ └────┘ └──┘
typ └────┘┴ └────┘┴ └──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴
st └────────┘└───────┘└────┘└──┘
687
688 @[simp] lemma mk_add_move_right_inl {xl xr yl yr} {xL xR yL yR} {i} :
doc └──┘
689 (mk xl xr xL xR + mk yl yr yL yR).move_right (sum.inl i) = (mk xl xr xL xR).move_right i + (mk yl yr yL yR) :=
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘
src └┘ ┴ └┘ └────────┘ └─────┘ ┴ └┘ └────────┘ ┴ └┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘
doc └────────┘ └────────┘
690 rfl
id └─┘
src └─┘
typ └─┘
691 @[simp] lemma add_move_right_inl {x y : pgame} {i} :
id └───┘
src └───┘
typ └───┘
doc └──┘ └───┘
692 (x + y).move_right ((@right_moves_add x y).symm (sum.inl i)) = x.move_right i + y :=
id ┴ ┴ ┴ └────────┘ └─────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴└─────────┘ ┴ ┴ ┴
src ┴ └────────┘ └─────────────┘ └──┘ └─────┘ ┴ └─────────┘ ┴
typ ┴ ┴ ┴ └────────┘ └─────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴└─────────┘ ┴ ┴ ┴
doc └────────┘ └─────────────┘ └─────────┘
693 by { cases x, cases y, refl, }
id ┴ ┴
src └────┘ └────┘ └──┘
typ └────┘┴ └────┘┴ └──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴
st └────────┘└───────┘└────┘└──┘
694
695 @[simp] lemma mk_add_move_left_inr {xl xr yl yr} {xL xR yL yR} {i} :
doc └──┘
696 (mk xl xr xL xR + mk yl yr yL yR).move_left (sum.inr i) = (mk xl xr xL xR) + (mk yl yr yL yR).move_left i :=
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ ┴
src └┘ ┴ └┘ └───────┘ └─────┘ ┴ └┘ ┴ └┘ └───────┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └───────┘ ┴
doc └───────┘ └───────┘
697 rfl
id └─┘
src └─┘
typ └─┘
698 @[simp] lemma add_move_left_inr {x y : pgame} {i : y.left_moves} :
id └───┘ ┴└─────────┘
src └───┘ └─────────┘
typ └───┘ ┴└─────────┘
doc └──┘ └───┘ └─────────┘
699 (x + y).move_left ((@left_moves_add x y).symm (sum.inr i)) = x + y.move_left i :=
id ┴ ┴ ┴ └───────┘ └────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴ ┴└────────┘ ┴
src ┴ └───────┘ └────────────┘ └──┘ └─────┘ ┴ ┴ └────────┘
typ ┴ ┴ ┴ └───────┘ └────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴ ┴└────────┘ ┴
doc └───────┘ └────────────┘ └────────┘
700 by { cases x, cases y, refl, }
id ┴ ┴
src └────┘ └────┘ └──┘
typ └────┘┴ └────┘┴ └──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴
st └────────┘└───────┘└────┘└──┘
701
702 @[simp] lemma mk_add_move_right_inr {xl xr yl yr} {xL xR yL yR} {i} :
doc └──┘
703 (mk xl xr xL xR + mk yl yr yL yR).move_right (sum.inr i) = (mk xl xr xL xR) + (mk yl yr yL yR).move_right i :=
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ ┴
src └┘ ┴ └┘ └────────┘ └─────┘ ┴ └┘ ┴ └┘ └────────┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └────────┘ ┴
doc └────────┘ └────────┘
704 rfl
id └─┘
src └─┘
typ └─┘
705 @[simp] lemma add_move_right_inr {x y : pgame} {i} :
id └───┘
src └───┘
typ └───┘
doc └──┘ └───┘
706 (x + y).move_right ((@right_moves_add x y).symm (sum.inr i)) = x + y.move_right i :=
id ┴ ┴ ┴ └────────┘ └─────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴ ┴└─────────┘ ┴
src ┴ └────────┘ └─────────────┘ └──┘ └─────┘ ┴ ┴ └─────────┘
typ ┴ ┴ ┴ └────────┘ └─────────────┘ ┴ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴ ┴└─────────┘ ┴
doc └────────┘ └─────────────┘ └─────────┘
707 by { cases x, cases y, refl, }
id ┴ ┴
src └────┘ └────┘ └──┘
typ └────┘┴ └────┘┴ └──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴
st └────────┘└───────┘└────┘└──┘
708
709 instance : has_sub pgame := ⟨λ x y, x + -y⟩
id └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴┴
src └─────┘ └───┘ ┴ ┴
typ └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴┴
doc └───┘
710
711 /-- `-(x+y)` has exactly the same moves as `-x + -y`. -/
712 def neg_add_relabelling : Π (x y : pgame), relabelling (-(x + y)) (-x + -y)
id ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └───┘ └─────────┘
713 | (mk xl xr xL xR) (mk yl yr yL yR) :=
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
714 ⟨equiv.refl _, equiv.refl _,
id └────────┘ └────────┘
src └────────┘ └────────┘
typ └────────┘ └────────┘
715 λ j, sum.cases_on j
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
716 (λ j, neg_add_relabelling (xR j) (mk yl yr yL yR))
id ┴ └─────────────────┘ ┴ └┘
src └┘
typ ┴ └─────────────────┘ ┴ └┘
717 (λ j, neg_add_relabelling (mk xl xr xL xR) (yR j)),
id ┴ └─────────────────┘ └┘ ┴
src └┘
typ ┴ └─────────────────┘ └┘ ┴
718 λ i, sum.cases_on i
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
719 (λ i, neg_add_relabelling (xL i) (mk yl yr yL yR))
id ┴ └─────────────────┘ ┴ └┘
src └┘
typ ┴ └─────────────────┘ ┴ └┘
720 (λ i, neg_add_relabelling (mk xl xr xL xR) (yL i))⟩
id ┴ └─────────────────┘ └┘ ┴
src └┘
typ ┴ └─────────────────┘ └┘ ┴
721 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
722
723 theorem neg_add_le {x y : pgame} : -(x + y) ≤ -x + -y :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └───┘
724 le_of_relabelling (neg_add_relabelling x y)
id └───────────────┘ └─────────────────┘ ┴ ┴
src └───────────────┘ └─────────────────┘
typ └───────────────┘ └─────────────────┘ ┴ ┴
doc └─────────────────┘
725
726 /-- `x+y` has exactly the same moves as `y+x`. -/
727 def add_comm_relabelling : Π (x y : pgame.{u}), relabelling (x + y) (y + x)
id ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────────┘ ┴ ┴
typ ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └─────────┘
728 | (mk xl xr xL xR) (mk yl yr yL yR) :=
id └┘
src └┘
typ └┘
729 begin
st └─────
730 refine ⟨equiv.sum_comm _ _, equiv.sum_comm _ _, _, _⟩,
id └────────────┘
src └─────┘ └────┘└────────────┘└─────────┘
typ └─────┘ └────┘└────────────┘└─────────┘
doc └─────┘ └────┘ └─────────┘
txt └─────┘ └────┘ └─────────┘
par └─────┘ └────┘ └─────────┘
pid ┴ └────┘ └─────────┘
st ──────────────────────────────────────────────────────┘└─
731 { rintros (_|_); { dsimp [left_moves_add], apply add_comm_relabelling, } },
id └────────────┘
src └───────────┘ └─────┘└────────────┘┴ └────┘
typ └───────────┘ └─────┘└────────────┘┴ └────┘
doc └───────────┘ └─────┘└────────────┘┴ └────┘
txt └───────────┘ └─────┘ ┴ └────┘
par └───────────┘ └─────┘ ┴ └────┘
pid └────┘ ┴┴ ┴ ┴
st ───┘└─────────────┘└──────────────────────┘└──────────────────────────┘└────┘└
732 { rintros (_|_); { dsimp [right_moves_add], apply add_comm_relabelling, } },
id └─────────────┘
src └───────────┘ └─────┘└─────────────┘┴ └────┘
typ └───────────┘ └─────┘└─────────────┘┴ └────┘
doc └───────────┘ └─────┘└─────────────┘┴ └────┘
txt └───────────┘ └─────┘ ┴ └────┘
par └───────────┘ └─────┘ ┴ └────┘
pid └────┘ ┴┴ ┴ ┴
st ──────────────────┘└───────────────────────┘└──────────────────────────┘└──────
733 end
st ──┘
734 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
735
736 theorem add_comm_le {x y : pgame} : x + y ≤ y + x :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
737 le_of_relabelling (add_comm_relabelling x y)
id └───────────────┘ └──────────────────┘ ┴ ┴
src └───────────────┘ └──────────────────┘
typ └───────────────┘ └──────────────────┘ ┴ ┴
doc └──────────────────┘
738
739 theorem add_comm_equiv {x y : pgame} : x + y ≈ y + x :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴
740 equiv_of_relabelling (add_comm_relabelling x y)
id └──────────────────┘ └──────────────────┘ ┴ ┴
src └──────────────────┘ └──────────────────┘
typ └──────────────────┘ └──────────────────┘ ┴ ┴
doc └──────────────────┘ └──────────────────┘
741
742 /-- `(x + y) + z` has exactly the same moves as `x + (y + z)`. -/
743 def add_assoc_relabelling : Π (x y z : pgame.{u}), relabelling ((x + y) + z) (x + (y + z))
id ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────────┘ ┴ ┴ ┴ ┴
typ ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └─────────┘
744 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
id └┘
src └┘
typ └┘
745 begin
st └─────
746 refine ⟨equiv.sum_assoc _ _ _, equiv.sum_assoc _ _ _, _, _⟩,
id └─────────────┘
src └─────┘ └──────┘└─────────────┘└───────────┘
typ └─────┘ └──────┘└─────────────┘└───────────┘
doc └─────┘ └──────┘ └───────────┘
txt └─────┘ └──────┘ └───────────┘
par └─────┘ └──────┘ └───────────┘
pid ┴ └──────┘ └───────────┘
st ────────────────────────────────────────────────────────────┘└─
747 { rintro (⟨i|i⟩|i),
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───┘└──────────────┘└─
748 { apply add_assoc_relabelling, },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└─────────────────────────┘└──┘└
749 { change relabelling
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘└─────────┘└
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────┘└──────────────────
750 (mk xl xr xL xR + yL i + mk zl zr zL zR) (mk xl xr xL xR + (yL i + mk zl zr zL zR)),
id ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src ───────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘┴ ┴ ┴ ┴ └┘
typ ───────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└┘┴└┘┴└┘┴└┘┴ ┴ └┘┴┴┴ ┴└┘┴└┘┴└┘┴└┘┴└┘└┘
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
751 apply add_assoc_relabelling, },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────┘└──┘└
752 { change relabelling
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘└─────────┘└
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────────
753 (mk xl xr xL xR + mk yl yr yL yR + zL i) (mk xl xr xL xR + (mk yl yr yL yR + zL i)),
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└┘┴└┘┴└┘┴└┘┴ ┴ └┘┴└┘┴└┘┴└┘┴└┘┴ ┴└┘┴┴└┘
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
754 apply add_assoc_relabelling, } },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────┘└────┘└
755 { rintro (j|⟨j|j⟩),
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───────────────────┘└─
756 { apply add_assoc_relabelling, },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└─────────────────────────┘└──┘└
757 { change relabelling
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘└─────────┘└
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────┘└──────────────────
758 (mk xl xr xL xR + yR j + mk zl zr zL zR) (mk xl xr xL xR + (yR j + mk zl zr zL zR)),
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘┴ ┴ ┴ ┴ └┘
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└┘┴└┘┴└┘┴└┘┴ ┴ └┘┴┴┴ ┴└┘┴└┘┴└┘┴└┘┴└┘└┘
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
759 apply add_assoc_relabelling, },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────┘└──┘└
760 { change relabelling
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘└─────────┘└
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────────
761 (mk xl xr xL xR + mk yl yr yL yR + zR j) (mk xl xr xL xR + (mk yl yr yL yR + zR j)),
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└┘┴└┘┴└┘┴└┘┴ ┴ └┘┴└┘┴└┘┴└┘┴└┘┴ ┴└┘┴┴└┘
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
762 apply add_assoc_relabelling, } },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────┘└──────
763 end
st ──┘
764 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
765
766 theorem add_assoc_equiv {x y z : pgame} : (x + y) + z ≈ x + (y + z) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴
767 equiv_of_relabelling (add_assoc_relabelling x y z)
id └──────────────────┘ └───────────────────┘ ┴ ┴ ┴
src └──────────────────┘ └───────────────────┘
typ └──────────────────┘ └───────────────────┘ ┴ ┴ ┴
doc └──────────────────┘ └───────────────────┘
768
769 theorem add_le_add_right : Π {x y z : pgame} (h : x ≤ y), x + z ≤ y + z
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
770 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
id └┘
src └┘
typ └┘
771 begin
st └─────
772 intros h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────┘└─
773 rw le_def,
id └────┘
src └─┘└────┘
typ └─┘└────┘
doc └─┘└────┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
774 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
775 { -- if Left plays first
st ───┘└──────────────────────
776 intros i,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ───────────┘└─
777 change xl ⊕ zl at i,
id └┘ ┴ └┘
src └─────┘ ┴┴┴ └───┘
typ └─────┘└┘┴┴┴└┘└───┘
doc └─────┘ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ └───┘
par └─────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴└──┘
st ──────────────────────┘└─
778 cases i,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────┘└─
779 { -- either they play in x
st ─────┘└────────────────────────
780 rw le_def at h,
id └────┘
src └─┘└────┘└───┘
typ └─┘└────┘└───┘
doc └─┘└────┘└───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────────────┘└─
781 cases h,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
782 have t := h_left i,
id └────┘ ┴
src └────────┘ ┴
typ └────────┘└────┘┴┴
doc └────────┘ ┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ───────────────────────┘└─
783 rcases t with ⟨i', ih⟩ | ⟨j, jh⟩,
id ┴
src └─────┘ └──────────────────────┘
typ └─────┘┴└──────────────────────┘
doc └─────┘ └──────────────────────┘
txt └─────┘ └──────────────────────┘
par └─────┘ └──────────────────────┘
pid ┴ └──────────────────────┘
st ─────────────────────────────────────┘└─
784 { left,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└──┘└─
785 refine ⟨(left_moves_add _ _).inv_fun (sum.inl i'), _⟩,
id └────────────┘ └─────┘ └┘
src └─────┘ └────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └────────────┘└────────────┘ └─────┘┴└┘└───┘
doc └─────┘ └────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ────────────────────────────────────────────────────────────┘└─
786 exact add_le_add_right ih, },
id └──────────────┘ └┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────┘└──┘└
787 { right,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────────┘└─
788 refine ⟨(right_moves_add _ _).inv_fun (sum.inl j), _⟩,
id └─────────────┘ └─────┘ ┴
src └─────┘ └─────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └─────────────┘└────────────┘ └─────┘┴┴└───┘
doc └─────┘ └─────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ────────────────────────────────────────────────────────────┘└─
789 convert add_le_add_right jh,
id └──────────────┘ └┘
src └──────┘└──────────────┘┴
typ └──────┘└──────────────┘┴└┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ──────────────────────────────────┘└─
790 apply add_move_right_inl },
id └────────────────┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────┘└──
791 },
st ───────┘└
792 { -- or play in z
st ──────────────────────
793 left,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────────┘└─
794 refine ⟨(left_moves_add _ _).inv_fun (sum.inr i), _⟩,
id └────────────┘ └─────┘ ┴
src └─────┘ └────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └────────────┘└────────────┘ └─────┘┴┴└───┘
doc └─────┘ └────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ─────────────────────────────────────────────────────────┘└─
795 exact add_le_add_right h, }, },
id └──────────────┘ ┴
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────┘└─────┘└
796 { -- if Right plays first
st ────────────────────────────
797 intros j,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ───────────┘└─
798 change yr ⊕ zr at j,
id └┘ └┘
src └─────┘ ┴ ┴ └───┘
typ └─────┘└┘┴ ┴└┘└───┘
doc └─────┘ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ └───┘
par └─────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴└──┘
st ──────────────────────┘└─
799 cases j,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────┘└─
800 { -- either they play in y
st ─────┘└────────────────────────
801 rw le_def at h,
id └────┘
src └─┘└────┘└───┘
typ └─┘└────┘└───┘
doc └─┘└────┘└───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────────────┘└─
802 cases h,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
803 have t := h_right j,
id └─────┘ ┴
src └────────┘ ┴
typ └────────┘└─────┘┴┴
doc └────────┘ ┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ────────────────────────┘└─
804 rcases t with ⟨i, ih⟩ | ⟨j', jh⟩,
id ┴
src └─────┘ └──────────────────────┘
typ └─────┘┴└──────────────────────┘
doc └─────┘ └──────────────────────┘
txt └─────┘ └──────────────────────┘
par └─────┘ └──────────────────────┘
pid ┴ └──────────────────────┘
st ─────────────────────────────────────┘└─
805 { left,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└──┘└─
806 refine ⟨(left_moves_add _ _).inv_fun (sum.inl i), _⟩,
id └────────────┘ └─────┘ ┴
src └─────┘ └────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └────────────┘└────────────┘ └─────┘┴┴└───┘
doc └─────┘ └────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ───────────────────────────────────────────────────────────┘└─
807 convert add_le_add_right ih,
id └──────────────┘ └┘
src └──────┘└──────────────┘┴
typ └──────┘└──────────────┘┴└┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ──────────────────────────────────┘└─
808 apply add_move_left_inl },
id └───────────────┘
src └────┘└───────────────┘┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────┘└┘└
809 { right,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────────┘└─
810 refine ⟨(right_moves_add _ _).inv_fun (sum.inl j'), _⟩,
id └─────────────┘ └─────┘ └┘
src └─────┘ └─────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └─────────────┘└────────────┘ └─────┘┴└┘└───┘
doc └─────┘ └─────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ─────────────────────────────────────────────────────────────┘└─
811 exact add_le_add_right jh } },
id └──────────────┘ └┘
src └────┘└──────────────┘┴ ┴
typ └────┘└──────────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────────┘└──┘└
812 { -- or play in z
st ──────────────────────
813 right,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
814 refine ⟨(right_moves_add _ _).inv_fun (sum.inr j), _⟩,
id └─────────────┘ └─────┘ ┴
src └─────┘ └─────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └─────────────┘└────────────┘ └─────┘┴┴└───┘
doc └─────┘ └─────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ──────────────────────────────────────────────────────────┘└─
815 exact add_le_add_right h } }
id └──────────────┘ ┴
src └────┘└──────────────┘┴ ┴
typ └────┘└──────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────┘└───
816 end
st ──┘
817 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
818
819 theorem add_le_add_left {x y z : pgame} (h : y ≤ z) : x + y ≤ x + z :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
820 calc x + y ≤ y + x : add_comm_le
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
src ┴ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
821 ... ≤ z + x : add_le_add_right h
id ┴ ┴ ┴ └──────────────┘ ┴
src ┴ └──────────────┘
typ ┴ ┴ ┴ └──────────────┘ ┴
822 ... ≤ x + z : add_comm_le
id ┴ ┴ ┴ └─────────┘
src ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘
823
824 theorem add_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w + y ≈ x + z :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ ┴ ┴ ┴
825 ⟨calc w + y ≤ w + z : add_le_add_left h₂.1
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └┘┴
src ┴ ┴ └─────────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └┘┴
826 ... ≤ x + z : add_le_add_right h₁.1,
id ┴ ┴ ┴ └──────────────┘ └┘┴
src ┴ └──────────────┘ ┴
typ ┴ ┴ ┴ └──────────────┘ └┘┴
827 calc x + z ≤ x + y : add_le_add_left h₂.2
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └┘┴
src ┴ ┴ └─────────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └┘┴
828 ... ≤ w + y : add_le_add_right h₁.2⟩
id ┴ ┴ ┴ └──────────────┘ └┘┴
src ┴ └──────────────┘ ┴
typ ┴ ┴ ┴ └──────────────┘ └┘┴
829
830 theorem add_left_neg_le_zero : Π {x : pgame}, (-x) + x ≤ 0
id ┴ └───┘ ┴┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ └───┘ ┴┴ ┴ ┴ ┴
doc └───┘
831 | ⟨xl, xr, xL, xR⟩ :=
832 begin
st └─────
833 rw [le_def],
id └────┘
src └──┘└────┘┴
typ └──┘└────┘┴
doc └──┘└────┘┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────┘└──
834 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
835 { intro i,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
836 change xr ⊕ xl at i,
id └┘ ┴ └┘
src └─────┘ ┴┴┴ └───┘
typ └─────┘└┘┴┴┴└┘└───┘
doc └─────┘ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ └───┘
par └─────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴└──┘
st ──────────────────────┘└─
837 cases i,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────┘└─
838 { -- If Left played in -x, Right responds with the same move in x.
st ─────┘└────────────────────────────────────────────────────────────────
839 right,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
840 refine ⟨(right_moves_add _ _).inv_fun (sum.inr i), _⟩,
id └─────────────┘ └─────┘ ┴
src └─────┘ └─────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └─────────────┘└────────────┘ └─────┘┴┴└───┘
doc └─────┘ └─────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ──────────────────────────────────────────────────────────┘└─
841 convert @add_left_neg_le_zero (xR i),
id └──────────────────┘ └┘ ┴
src └──────┘ ┴ ┴ ┴
typ └──────┘ └──────────────────┘┴ └┘┴┴┴
doc └──────┘ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
842 exact add_move_right_inr },
id └────────────────┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘└┘└
843 { -- If Left in x, Right responds with the same move in -x.
st ────────────────────────────────────────────────────────────────
844 right,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
845 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
846 refine ⟨(right_moves_add _ _).inv_fun (sum.inl i), _⟩,
id └─────────────┘ └─────┘ ┴
src └─────┘ └─────────────┘└────────────┘ └─────┘┴ └───┘
typ └─────┘ └─────────────┘└────────────┘ └─────┘┴┴└───┘
doc └─────┘ └─────────────┘└────────────┘ ┴ └───┘
txt └─────┘ └────────────┘ ┴ └───┘
par └─────┘ └────────────┘ ┴ └───┘
pid ┴ └────────────┘ ┴ └───┘
st ──────────────────────────────────────────────────────────┘└─
847 convert @add_left_neg_le_zero (xL i),
id └──────────────────┘ └┘ ┴
src └──────┘ ┴ ┴ ┴
typ └──────┘ └──────────────────┘┴ └┘┴┴┴
doc └──────┘ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
848 exact add_move_right_inl }, },
id └────────────────┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘└───┘└
849 { rintro ⟨⟩, }
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └─┘
st ────────────┘└───
850 end
st ──┘
851 using_well_founded { dec_tac := pgame_wf_tac }
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
852
853 theorem zero_le_add_left_neg : Π {x : pgame}, 0 ≤ (-x) + x :=
id └───┘ ┴ ┴┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴┴ ┴ ┴
doc └───┘
854 begin
st └─────
855 intro x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
856 rw [le_iff_neg_ge, neg_zero],
id └───────────┘ └──────┘
src └──┘└───────────┘└┘└──────┘┴
typ └──┘└───────────┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────┘└────────┘└──
857 exact le_trans neg_add_le add_left_neg_le_zero
id └──────┘ └────────┘ └──────────────────┘
src └────┘└──────┘┴└────────┘┴└──────────────────┘┴
typ └────┘└──────┘┴└────────┘┴└──────────────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────┘
858 end
st └─┘
859
860 theorem add_left_neg_equiv {x : pgame} : (-x) + x ≈ 0 :=
id └───┘ ┴┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴┴ ┴ ┴ ┴
doc └───┘ ┴
861 ⟨add_left_neg_le_zero, zero_le_add_left_neg⟩
id └──────────────────┘ └──────────────────┘
src └──────────────────┘ └──────────────────┘
typ └──────────────────┘ └──────────────────┘
862
863 theorem add_right_neg_le_zero {x : pgame} : x + (-x) ≤ 0 :=
id └───┘ ┴ ┴ ┴┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴┴ ┴
doc └───┘
864 calc x + (-x) ≤ (-x) + x : add_comm_le
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────────┘
src ┴ ┴ ┴ ┴ └─────────┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────────┘
865 ... ≤ 0 : add_left_neg_le_zero
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
866
867 theorem zero_le_add_right_neg {x : pgame} : 0 ≤ x + (-x) :=
id └───┘ ┴ ┴ ┴ ┴┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴┴
doc └───┘
868 calc 0 ≤ (-x) + x : zero_le_add_left_neg
id ┴┴ ┴ ┴ └──────────────────┘
src ┴ ┴ └──────────────────┘
typ ┴┴ ┴ ┴ └──────────────────┘
869 ... ≤ x + (-x) : add_comm_le
id ┴ ┴ ┴┴ └─────────┘
src ┴ ┴ └─────────┘
typ ┴ ┴ ┴┴ └─────────┘
870
871 theorem add_lt_add_right {x y z : pgame} (h : x < y) : x + z < y + z :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
872 suffices y + z ≤ x + z → y ≤ x, by { rw ←not_le at ⊢ h, exact mt this h },
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └┘ └──┘ ┴
src ┴ ┴ ┴ ┴ └──┘└────┘└─────┘ └────┘└┘┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└────┘└─────┘ └────┘└┘┴└──┘┴┴┴
doc └──┘ └─────┘ └────┘ ┴ ┴ ┴
txt └──┘ └─────┘ └────┘ ┴ ┴ ┴
par └──┘ └─────┘ └────┘ ┴ ┴ ┴
pid └┘ └─────┘ ┴ ┴ ┴ ┴
st └──────────────────┘└────────────────┘└┘
873 assume w,
id ┴
typ ┴
874 calc y ≤ y + 0 : le_of_relabelling (add_zero_relabelling _).symm
id ┴ ┴ ┴ └───────────────┘ └──────────────────┘ └──┘
src ┴ └───────────────┘ └──────────────────┘ └──┘
typ ┴ ┴ ┴ └───────────────┘ └──────────────────┘ └──┘
doc └──────────────────┘ └──┘
875 ... ≤ y + (z + -z) : add_le_add_left zero_le_add_right_neg
id ┴ ┴ ┴ ┴ ┴┴ └─────────────┘ └───────────────────┘
src ┴ ┴ ┴ └─────────────┘ └───────────────────┘
typ ┴ ┴ ┴ ┴ ┴┴ └─────────────┘ └───────────────────┘
876 ... ≤ (y + z) + (-z) : le_of_relabelling (add_assoc_relabelling _ _ _).symm
id ┴ ┴ ┴ ┴ ┴┴ └───────────────┘ └───────────────────┘ └──┘
src ┴ ┴ ┴ └───────────────┘ └───────────────────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴┴ └───────────────┘ └───────────────────┘ └──┘
doc └───────────────────┘ └──┘
877 ... ≤ (x + z) + (-z) : add_le_add_right w
id ┴ ┴ ┴ ┴ ┴┴ └──────────────┘ ┴
src ┴ ┴ ┴ └──────────────┘
typ ┴ ┴ ┴ ┴ ┴┴ └──────────────┘ ┴
878 ... ≤ x + (z + -z) : le_of_relabelling (add_assoc_relabelling _ _ _)
id ┴ ┴ ┴ ┴ ┴┴ └───────────────┘ └───────────────────┘
src ┴ ┴ ┴ └───────────────┘ └───────────────────┘
typ ┴ ┴ ┴ ┴ ┴┴ └───────────────┘ └───────────────────┘
doc └───────────────────┘
879 ... ≤ x + 0 : add_le_add_left add_right_neg_le_zero
id ┴ ┴ └─────────────┘ └───────────────────┘
src ┴ └─────────────┘ └───────────────────┘
typ ┴ ┴ └─────────────┘ └───────────────────┘
880 ... ≤ x : le_of_relabelling (add_zero_relabelling _)
id ┴ └───────────────┘ └──────────────────┘
src └───────────────┘ └──────────────────┘
typ ┴ └───────────────┘ └──────────────────┘
doc └──────────────────┘
881
882 theorem add_lt_add_left {x y z : pgame} (h : y < z) : x + y < x + z :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
883 calc x + y ≤ y + x : add_comm_le
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
src ┴ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
884 ... < z + x : add_lt_add_right h
id ┴ ┴ ┴ └──────────────┘ ┴
src ┴ └──────────────┘
typ ┴ ┴ ┴ └──────────────┘ ┴
885 ... ≤ x + z : add_comm_le
id ┴ ┴ ┴ └─────────┘
src ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘
886
887 theorem le_iff_sub_nonneg {x y : pgame} : x ≤ y ↔ 0 ≤ y - x :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
888 ⟨λ h, le_trans zero_le_add_right_neg (add_le_add_right h),
id ┴ └──────┘ └───────────────────┘ └──────────────┘ ┴
src └──────┘ └───────────────────┘ └──────────────┘
typ ┴ └──────┘ └───────────────────┘ └──────────────┘ ┴
889 λ h,
id ┴
typ ┴
890 calc x ≤ 0 + x : le_of_relabelling (zero_add_relabelling x).symm
id ┴ ┴ ┴ └───────────────┘ └──────────────────┘ ┴ └──┘
src ┴ └───────────────┘ └──────────────────┘ └──┘
typ ┴ ┴ ┴ └───────────────┘ └──────────────────┘ ┴ └──┘
doc └──────────────────┘ └──┘
891 ... ≤ (y - x) + x : add_le_add_right h
id ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴
src ┴ ┴ └──────────────┘
typ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴
892 ... ≤ y + (-x + x) : le_of_relabelling (add_assoc_relabelling _ _ _)
id ┴ ┴ ┴┴ ┴ ┴ └───────────────┘ └───────────────────┘
src ┴ ┴ ┴ └───────────────┘ └───────────────────┘
typ ┴ ┴ ┴┴ ┴ ┴ └───────────────┘ └───────────────────┘
doc └───────────────────┘
893 ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero)
id ┴ ┴ └─────────────┘ └──────────────────┘
src ┴ └─────────────┘ └──────────────────┘
typ ┴ ┴ └─────────────┘ └──────────────────┘
894 ... ≤ y : le_of_relabelling (add_zero_relabelling y)⟩
id ┴ └───────────────┘ └──────────────────┘ ┴
src └───────────────┘ └──────────────────┘
typ ┴ └───────────────┘ └──────────────────┘ ┴
doc └──────────────────┘
895 theorem lt_iff_sub_pos {x y : pgame} : x < y ↔ 0 < y - x :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
896 ⟨λ h, lt_of_le_of_lt zero_le_add_right_neg (add_lt_add_right h),
id ┴ └────────────┘ └───────────────────┘ └──────────────┘ ┴
src └────────────┘ └───────────────────┘ └──────────────┘
typ ┴ └────────────┘ └───────────────────┘ └──────────────┘ ┴
897 λ h,
id ┴
typ ┴
898 calc x ≤ 0 + x : le_of_relabelling (zero_add_relabelling x).symm
id ┴ ┴ ┴ └───────────────┘ └──────────────────┘ ┴ └──┘
src ┴ └───────────────┘ └──────────────────┘ └──┘
typ ┴ ┴ ┴ └───────────────┘ └──────────────────┘ ┴ └──┘
doc └──────────────────┘ └──┘
899 ... < (y - x) + x : add_lt_add_right h
id ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴
src ┴ ┴ └──────────────┘
typ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴
900 ... ≤ y + (-x + x) : le_of_relabelling (add_assoc_relabelling _ _ _)
id ┴ ┴ ┴┴ ┴ ┴ └───────────────┘ └───────────────────┘
src ┴ ┴ ┴ └───────────────┘ └───────────────────┘
typ ┴ ┴ ┴┴ ┴ ┴ └───────────────┘ └───────────────────┘
doc └───────────────────┘
901 ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero)
id ┴ ┴ └─────────────┘ └──────────────────┘
src ┴ └─────────────┘ └──────────────────┘
typ ┴ ┴ └─────────────┘ └──────────────────┘
902 ... ≤ y : le_of_relabelling (add_zero_relabelling y)⟩
id ┴ └───────────────┘ └──────────────────┘ ┴
src └───────────────┘ └──────────────────┘
typ ┴ └───────────────┘ └──────────────────┘ ┴
doc └──────────────────┘
903
904 /-- The pre-game `star`, which is fuzzy/confused with zero. -/
905 def star : pgame := pgame.of_lists [0] [0]
id └───┘ └────────────┘ ┴ ┴ ┴ ┴
src └───┘ └────────────┘ ┴ ┴ ┴ ┴
typ └───┘ └────────────┘ ┴ ┴ ┴ ┴
doc └───┘ └────────────┘
906
907 theorem star_lt_zero : star < 0 :=
id └──┘ ┴
src └──┘ ┴
typ └──┘ ┴
doc └──┘
908 or.inr ⟨⟨0, zero_lt_one⟩, (by split; rintros ⟨⟩)⟩
id └────┘ └─────────┘
src └────┘ └─────────┘ └───┘ └────────┘
typ └────┘ └─────────┘ └───┘ └────────┘
doc └───┘ └────────┘
txt └───┘ └────────┘
par └───┘ └────────┘
pid └─┘
st └────────────────┘
909
910 theorem zero_lt_star : 0 < star :=
id ┴ └──┘
src ┴ └──┘
typ ┴ └──┘
doc └──┘
911 or.inl ⟨⟨0, zero_lt_one⟩, (by split; rintros ⟨⟩)⟩
id └────┘ └─────────┘
src └────┘ └─────────┘ └───┘ └────────┘
typ └────┘ └─────────┘ └───┘ └────────┘
doc └───┘ └────────┘
txt └───┘ └────────┘
par └───┘ └────────┘
pid └─┘
st └────────────────┘
912
913 /-- The pre-game `ω`. (In fact all ordinals have game and surreal representatives.) -/
914 def omega : pgame := ⟨ulift ℕ, pempty, λ n, ↑n.1, pempty.elim⟩
id └───┘ └───┘ ┴ └────┘ ┴ ┴┴┴ └─────────┘
src └───┘ └───┘ ┴ └────┘ ┴ ┴ └─────────┘
typ └───┘ └───┘ ┴ └────┘ ┴ ┴┴┴ └─────────┘
doc └───┘ └───┘ └────┘
915
916 end pgame